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

Metamath Proof Explorer

Theorem inex1g

Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995)

Ref Expression
Assertion inex1g ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 ineq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∩ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
2 1 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∩ 𝐵 ) ∈ V ↔ ( 𝐴 ∩ 𝐵 ) ∈ V ) )
3 vex ⊢ 𝑥 ∈ V
4 3 inex1 ⊢ ( 𝑥 ∩ 𝐵 ) ∈ V
5 2 4 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )