Metamath Proof Explorer

Theorem inex1

Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of TakeutiZaring p. 22. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis inex1.1 ⊢ A ∈ V
Assertion inex1 ⊢ A ∩ B ∈ V

Proof

Step Hyp Ref Expression
1 inex1.1 ⊢ A ∈ V
2 1 sepgi ⊢ ∃ x ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
3 dfcleq ⊢ x = A ∩ B ↔ ∀ y y ∈ x ↔ y ∈ A ∩ B
4 elin ⊢ y ∈ A ∩ B ↔ y ∈ A ∧ y ∈ B
5 4 bibi2i ⊢ y ∈ x ↔ y ∈ A ∩ B ↔ y ∈ x ↔ y ∈ A ∧ y ∈ B
6 5 albii ⊢ ∀ y y ∈ x ↔ y ∈ A ∩ B ↔ ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
7 3 6 bitri ⊢ x = A ∩ B ↔ ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
8 7 exbii ⊢ ∃ x x = A ∩ B ↔ ∃ x ∀ y y ∈ x ↔ y ∈ A ∧ y ∈ B
9 2 8 mpbir ⊢ ∃ x x = A ∩ B
10 9 issetri ⊢ A ∩ B ∈ V