Metamath Proof Explorer


Theorem riin0

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

Ref Expression
Assertion riin0 X=AxXS=A

Proof

Step Hyp Ref Expression
1 iineq1 X=xXS=xS
2 1 ineq2d X=AxXS=AxS
3 0iin xS=V
4 3 ineq2i AxS=AV
5 inv1 AV=A
6 4 5 eqtri AxS=A
7 2 6 eqtrdi X=AxXS=A