Metamath Proof Explorer

Theorem eliin2f

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis eliin2f.1 
|- F/_ x B
Assertion eliin2f 
|- ( B =/= (/) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )

Proof

Step Hyp Ref Expression
1 eliin2f.1 
 |-  F/_ x B
2 eliin 
 |-  ( A e. _V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
3 2 adantl 
 |-  ( ( B =/= (/) /\ A e. _V ) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
4 prcnel 
 |-  ( -. A e. _V -> -. A e. |^|_ x e. B C )
5 4 adantl 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> -. A e. |^|_ x e. B C )
6 n0 
 |-  ( B =/= (/) <-> E. y y e. B )
7 6 birani 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> E. y y e. B )
8 prcnel 
 |-  ( -. A e. _V -> -. A e. [_ y / x ]_ C )
9 8 a1d 
 |-  ( -. A e. _V -> ( y e. B -> -. A e. [_ y / x ]_ C ) )
10 9 adantl 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> ( y e. B -> -. A e. [_ y / x ]_ C ) )
11 10 ancld 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> ( y e. B -> ( y e. B /\ -. A e. [_ y / x ]_ C ) ) )
12 11 eximdv 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> ( E. y y e. B -> E. y ( y e. B /\ -. A e. [_ y / x ]_ C ) ) )
13 7 12 mpd 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> E. y ( y e. B /\ -. A e. [_ y / x ]_ C ) )
14 df-rex 
 |-  ( E. y e. B -. A e. [_ y / x ]_ C <-> E. y ( y e. B /\ -. A e. [_ y / x ]_ C ) )
15 13 14 sylibr 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> E. y e. B -. A e. [_ y / x ]_ C )
16 nfcv 
 |-  F/_ y B
17 nfv 
 |-  F/ y -. A e. C
18 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
19 18 nfel2 
 |-  F/ x A e. [_ y / x ]_ C
20 19 nfn 
 |-  F/ x -. A e. [_ y / x ]_ C
21 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
22 21 eleq2d 
 |-  ( x = y -> ( A e. C <-> A e. [_ y / x ]_ C ) )
23 22 notbid 
 |-  ( x = y -> ( -. A e. C <-> -. A e. [_ y / x ]_ C ) )
24 1 16 17 20 23 cbvrexfw 
 |-  ( E. x e. B -. A e. C <-> E. y e. B -. A e. [_ y / x ]_ C )
25 15 24 sylibr 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> E. x e. B -. A e. C )
26 rexnal 
 |-  ( E. x e. B -. A e. C <-> -. A. x e. B A e. C )
27 25 26 sylib 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> -. A. x e. B A e. C )
28 5 27 2falsed 
 |-  ( ( B =/= (/) /\ -. A e. _V ) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )
29 3 28 pm2.61dan 
 |-  ( B =/= (/) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )