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

Metamath Proof Explorer

Theorem iinvdif

Description: The indexed intersection of a complement. (Contributed by Gérard Lang, 5-Aug-2018)

Ref Expression
Assertion iinvdif 
|- |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B )

Proof

Step Hyp Ref Expression
1 dif0 
 |-  ( _V \ (/) ) = _V
2 0iun 
 |-  U_ x e. (/) B = (/)
3 2 difeq2i 
 |-  ( _V \ U_ x e. (/) B ) = ( _V \ (/) )
4 0iin 
 |-  |^|_ x e. (/) ( _V \ B ) = _V
5 1 3 4 3eqtr4ri 
 |-  |^|_ x e. (/) ( _V \ B ) = ( _V \ U_ x e. (/) B )
6 iineq1 
 |-  ( A = (/) -> |^|_ x e. A ( _V \ B ) = |^|_ x e. (/) ( _V \ B ) )
7 iuneq1 
 |-  ( A = (/) -> U_ x e. A B = U_ x e. (/) B )
8 7 difeq2d 
 |-  ( A = (/) -> ( _V \ U_ x e. A B ) = ( _V \ U_ x e. (/) B ) )
9 5 6 8 3eqtr4a 
 |-  ( A = (/) -> |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B ) )
10 iindif2 
 |-  ( A =/= (/) -> |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B ) )
11 9 10 pm2.61ine 
 |-  |^|_ x e. A ( _V \ B ) = ( _V \ U_ x e. A B )