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