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	sepgi	⊢ ∃ 𝑥 ∀ 𝑦 ( 𝑦 ∈ 𝑥 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
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