How to use agda almost without data, only with postulates?

module sets where

postulate
    𝕊 : Set
    _∈_ : 𝕊 → 𝕊 → Set
infix 50 _∈_

data _and_ : Set → Set → Set where
    _∧_ : (x y : Set) → x and y
infixl 40 _and_
infixl 40 _∧_

data _≡_ : Set → Set → Set where
    _eq_ : (a b : Set) → a → b and b → a → a ≡ b
infixr 30 _≡_
infixr 30 _eq_

postulate
    _==_ : 𝕊 → 𝕊 → Set
    ==-def : (x y z : 𝕊) → ((z ∈ x ≡ z ∈ y) ≡ x == y)
infixr 50 _==_

postulate
    eq_ax : (x y : 𝕊) → (x == y) → (z : 𝕊) → (x ∈ z ≡ y ∈ z)
    ∃ : (x : Set) → (z : x → Set) → Set
    ∃-def : (x : Set) → (y : x) → (z : x → Set) → (z y ≡ ∃ x z)
    pair_ax : (x y : 𝕊) → ∃ 𝕊 λ { z → x ∈ z and y ∈ z }
    ∪ : 𝕊 → 𝕊
    ∪_def : (x y : 𝕊) → x ∈ ∪ y ≡ ∃ 𝕊 λ { z → x ∈ z and z ∈ y }
    _⊆_ : 𝕊 → 𝕊 → Set
    ⊆-def : (x y : 𝕊) → ((z : 𝕊) → z ∈ x → z ∈ y) ≡ x ⊆ y
infixl 50 _⊆_

first-proof : (x y : 𝕊) → x ⊆ y → (∪ x) ⊆ (∪ y)
first-proof x y z = {!!}

I am new to Agda. I try to find something that can verify my evidence. And so far Agda seems to be the best option (but still not enough convenient). I am implementing ZFC. And don't know, how to proof the last sentence.

I expect to proof without data, closest to the usual proof with quantifiers and connectives.