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

Metamath Proof Explorer

Theorem inex2g

Description: Sufficient condition for an intersection to be a set. Commuted form of inex1g . (Contributed by Peter Mazsa, 19-Dec-2018)

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

Proof

Step Hyp Ref Expression
1 incom ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
2 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝐵 ) ∈ V )
3 1 2 eqeltrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 ∩ 𝐴 ) ∈ V )