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

Metamath Proof Explorer

Theorem iindif2f

Description: Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws". (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypotheses iindif2f.1 
|- F/_ x A
iindif2f.2 
|- F/_ x B
Assertion iindif2f 
|- ( A =/= (/) -> |^|_ x e. A ( B \ C ) = ( B \ U_ x e. A C ) )

Proof

Step Hyp Ref Expression
1 iindif2f.1 
 |-  F/_ x A
2 iindif2f.2 
 |-  F/_ x B
3 2 nfcri 
 |-  F/ x y e. B
4 3 1 r19.28zf 
 |-  ( A =/= (/) -> ( A. x e. A ( y e. B /\ -. y e. C ) <-> ( y e. B /\ A. x e. A -. y e. C ) ) )
5 eldif 
 |-  ( y e. ( B \ C ) <-> ( y e. B /\ -. y e. C ) )
6 5 bicomi 
 |-  ( ( y e. B /\ -. y e. C ) <-> y e. ( B \ C ) )
7 6 ralbii 
 |-  ( A. x e. A ( y e. B /\ -. y e. C ) <-> A. x e. A y e. ( B \ C ) )
8 ralnex 
 |-  ( A. x e. A -. y e. C <-> -. E. x e. A y e. C )
9 eliun 
 |-  ( y e. U_ x e. A C <-> E. x e. A y e. C )
10 8 9 xchbinxr 
 |-  ( A. x e. A -. y e. C <-> -. y e. U_ x e. A C )
11 10 anbi2i 
 |-  ( ( y e. B /\ A. x e. A -. y e. C ) <-> ( y e. B /\ -. y e. U_ x e. A C ) )
12 4 7 11 3bitr3g 
 |-  ( A =/= (/) -> ( A. x e. A y e. ( B \ C ) <-> ( y e. B /\ -. y e. U_ x e. A C ) ) )
13 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A ( B \ C ) <-> A. x e. A y e. ( B \ C ) ) )
14 13 elv 
 |-  ( y e. |^|_ x e. A ( B \ C ) <-> A. x e. A y e. ( B \ C ) )
15 eldif 
 |-  ( y e. ( B \ U_ x e. A C ) <-> ( y e. B /\ -. y e. U_ x e. A C ) )
16 12 14 15 3bitr4g 
 |-  ( A =/= (/) -> ( y e. |^|_ x e. A ( B \ C ) <-> y e. ( B \ U_ x e. A C ) ) )
17 16 eqrdv 
 |-  ( A =/= (/) -> |^|_ x e. A ( B \ C ) = ( B \ U_ x e. A C ) )