Metamath Proof Explorer


Theorem riin0

Description: Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion riin0 ( 𝑋 = ∅ → ( 𝐴 𝑥𝑋 𝑆 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 iineq1 ( 𝑋 = ∅ → 𝑥𝑋 𝑆 = 𝑥 ∈ ∅ 𝑆 )
2 1 ineq2d ( 𝑋 = ∅ → ( 𝐴 𝑥𝑋 𝑆 ) = ( 𝐴 𝑥 ∈ ∅ 𝑆 ) )
3 0iin 𝑥 ∈ ∅ 𝑆 = V
4 3 ineq2i ( 𝐴 𝑥 ∈ ∅ 𝑆 ) = ( 𝐴 ∩ V )
5 inv1 ( 𝐴 ∩ V ) = 𝐴
6 4 5 eqtri ( 𝐴 𝑥 ∈ ∅ 𝑆 ) = 𝐴
7 2 6 eqtrdi ( 𝑋 = ∅ → ( 𝐴 𝑥𝑋 𝑆 ) = 𝐴 )