Metamath Proof Explorer

Theorem 0iin

Description: An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005)

Ref Expression
Assertion 0iin 
|- |^|_ x e. (/) A = _V

Proof

Step Hyp Ref Expression
1 df-iin 
 |-  |^|_ x e. (/) A = { y | A. x e. (/) y e. A }
2 vex 
 |-  y e. _V
3 ral0 
 |-  A. x e. (/) y e. A
4 2 3 2th 
 |-  ( y e. _V <-> A. x e. (/) y e. A )
5 4 abbi2i 
 |-  _V = { y | A. x e. (/) y e. A }
6 1 5 eqtr4i 
 |-  |^|_ x e. (/) A = _V