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 ) )