Metamath Proof Explorer

Theorem iindif1

Description: Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Assertion iindif1 
|- ( A =/= (/) -> |^|_ x e. A ( B \ C ) = ( |^|_ x e. A B \ C ) )

Proof

Step Hyp Ref Expression
1 r19.27zv 
 |-  ( A =/= (/) -> ( A. x e. A ( y e. B /\ -. y e. C ) <-> ( A. x e. A y e. B /\ -. y e. C ) ) )
2 eldif 
 |-  ( y e. ( B \ C ) <-> ( y e. B /\ -. y e. C ) )
3 2 ralbii 
 |-  ( A. x e. A y e. ( B \ C ) <-> A. x e. A ( y e. B /\ -. y e. C ) )
4 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
5 4 elv 
 |-  ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
6 5 anbi1i 
 |-  ( ( y e. |^|_ x e. A B /\ -. y e. C ) <-> ( A. x e. A y e. B /\ -. y e. C ) )
7 1 3 6 3bitr4g 
 |-  ( A =/= (/) -> ( A. x e. A y e. ( B \ C ) <-> ( y e. |^|_ x e. A B /\ -. y e. C ) ) )
8 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A ( B \ C ) <-> A. x e. A y e. ( B \ C ) ) )
9 8 elv 
 |-  ( y e. |^|_ x e. A ( B \ C ) <-> A. x e. A y e. ( B \ C ) )
10 eldif 
 |-  ( y e. ( |^|_ x e. A B \ C ) <-> ( y e. |^|_ x e. A B /\ -. y e. C ) )
11 7 9 10 3bitr4g 
 |-  ( A =/= (/) -> ( y e. |^|_ x e. A ( B \ C ) <-> y e. ( |^|_ x e. A B \ C ) ) )
12 11 eqrdv 
 |-  ( A =/= (/) -> |^|_ x e. A ( B \ C ) = ( |^|_ x e. A B \ C ) )