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 )