This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
Assertion inex1 ( 𝐴 ∩ 𝐵 ) ∈ V

Proof

Step Hyp Ref Expression
1 inex1.1 ⊢ 𝐴 ∈ V
2 1 zfauscl ⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
3 dfcleq ⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) )
4 elin ⊢ ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
5 4 bibi2i ⊢ ( ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
6 5 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
7 3 6 bitri ⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
8 7 exbii ⊢ ( ∃ 𝑥 𝑥 = ( 𝐴 ∩ 𝐵 ) ↔ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
9 2 8 mpbir ⊢ ∃ 𝑥 𝑥 = ( 𝐴 ∩ 𝐵 )
10 9 issetri ⊢ ( 𝐴 ∩ 𝐵 ) ∈ V