Metamath Proof Explorer

Theorem elmapintrab

Description: Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020)

Ref Expression
Hypotheses elmapintrab.ex 
|- C e. _V
elmapintrab.sub 
|- C C_ B
Assertion elmapintrab 
|- ( A e. V -> ( A e. |^| { w e. ~P B | E. x ( w = C /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) ) )

Proof

Step Hyp Ref Expression
1 elmapintrab.ex 
 |-  C e. _V
2 elmapintrab.sub 
 |-  C C_ B
3 elintrabg 
 |-  ( A e. V -> ( A e. |^| { w e. ~P B | E. x ( w = C /\ ph ) } <-> A. w e. ~P B ( E. x ( w = C /\ ph ) -> A e. w ) ) )
4 df-ral 
 |-  ( A. w e. ~P B ( E. x ( w = C /\ ph ) -> A e. w ) <-> A. w ( w e. ~P B -> ( E. x ( w = C /\ ph ) -> A e. w ) ) )
5 3 4 bitrdi 
 |-  ( A e. V -> ( A e. |^| { w e. ~P B | E. x ( w = C /\ ph ) } <-> A. w ( w e. ~P B -> ( E. x ( w = C /\ ph ) -> A e. w ) ) ) )
6 velpw 
 |-  ( w e. ~P B <-> w C_ B )
7 19.23v 
 |-  ( A. x ( ( w = C /\ ph ) -> A e. w ) <-> ( E. x ( w = C /\ ph ) -> A e. w ) )
8 7 bicomi 
 |-  ( ( E. x ( w = C /\ ph ) -> A e. w ) <-> A. x ( ( w = C /\ ph ) -> A e. w ) )
9 6 8 imbi12i 
 |-  ( ( w e. ~P B -> ( E. x ( w = C /\ ph ) -> A e. w ) ) <-> ( w C_ B -> A. x ( ( w = C /\ ph ) -> A e. w ) ) )
10 19.21v 
 |-  ( A. x ( w C_ B -> ( ( w = C /\ ph ) -> A e. w ) ) <-> ( w C_ B -> A. x ( ( w = C /\ ph ) -> A e. w ) ) )
11 bi2.04 
 |-  ( ( w C_ B -> ( ( w = C /\ ph ) -> A e. w ) ) <-> ( ( w = C /\ ph ) -> ( w C_ B -> A e. w ) ) )
12 impexp 
 |-  ( ( ( w = C /\ ph ) -> ( w C_ B -> A e. w ) ) <-> ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) )
13 11 12 bitri 
 |-  ( ( w C_ B -> ( ( w = C /\ ph ) -> A e. w ) ) <-> ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) )
14 13 albii 
 |-  ( A. x ( w C_ B -> ( ( w = C /\ ph ) -> A e. w ) ) <-> A. x ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) )
15 9 10 14 3bitr2i 
 |-  ( ( w e. ~P B -> ( E. x ( w = C /\ ph ) -> A e. w ) ) <-> A. x ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) )
16 15 albii 
 |-  ( A. w ( w e. ~P B -> ( E. x ( w = C /\ ph ) -> A e. w ) ) <-> A. w A. x ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) )
17 alcom 
 |-  ( A. w A. x ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) <-> A. x A. w ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) )
18 sseq1 
 |-  ( w = C -> ( w C_ B <-> C C_ B ) )
19 eleq2 
 |-  ( w = C -> ( A e. w <-> A e. C ) )
20 2 sseli 
 |-  ( A e. C -> A e. B )
21 20 pm4.71ri 
 |-  ( A e. C <-> ( A e. B /\ A e. C ) )
22 19 21 bitrdi 
 |-  ( w = C -> ( A e. w <-> ( A e. B /\ A e. C ) ) )
23 18 22 imbi12d 
 |-  ( w = C -> ( ( w C_ B -> A e. w ) <-> ( C C_ B -> ( A e. B /\ A e. C ) ) ) )
24 23 imbi2d 
 |-  ( w = C -> ( ( ph -> ( w C_ B -> A e. w ) ) <-> ( ph -> ( C C_ B -> ( A e. B /\ A e. C ) ) ) ) )
25 1 24 ceqsalv 
 |-  ( A. w ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) <-> ( ph -> ( C C_ B -> ( A e. B /\ A e. C ) ) ) )
26 bi2.04 
 |-  ( ( ph -> ( C C_ B -> ( A e. B /\ A e. C ) ) ) <-> ( C C_ B -> ( ph -> ( A e. B /\ A e. C ) ) ) )
27 pm5.5 
 |-  ( C C_ B -> ( ( C C_ B -> ( ph -> ( A e. B /\ A e. C ) ) ) <-> ( ph -> ( A e. B /\ A e. C ) ) ) )
28 2 27 ax-mp 
 |-  ( ( C C_ B -> ( ph -> ( A e. B /\ A e. C ) ) ) <-> ( ph -> ( A e. B /\ A e. C ) ) )
29 jcab 
 |-  ( ( ph -> ( A e. B /\ A e. C ) ) <-> ( ( ph -> A e. B ) /\ ( ph -> A e. C ) ) )
30 28 29 bitri 
 |-  ( ( C C_ B -> ( ph -> ( A e. B /\ A e. C ) ) ) <-> ( ( ph -> A e. B ) /\ ( ph -> A e. C ) ) )
31 25 26 30 3bitri 
 |-  ( A. w ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) <-> ( ( ph -> A e. B ) /\ ( ph -> A e. C ) ) )
32 31 albii 
 |-  ( A. x A. w ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) <-> A. x ( ( ph -> A e. B ) /\ ( ph -> A e. C ) ) )
33 19.26 
 |-  ( A. x ( ( ph -> A e. B ) /\ ( ph -> A e. C ) ) <-> ( A. x ( ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) )
34 19.23v 
 |-  ( A. x ( ph -> A e. B ) <-> ( E. x ph -> A e. B ) )
35 34 anbi1i 
 |-  ( ( A. x ( ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) )
36 32 33 35 3bitri 
 |-  ( A. x A. w ( w = C -> ( ph -> ( w C_ B -> A e. w ) ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) )
37 16 17 36 3bitri 
 |-  ( A. w ( w e. ~P B -> ( E. x ( w = C /\ ph ) -> A e. w ) ) <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) )
38 5 37 bitrdi 
 |-  ( A e. V -> ( A e. |^| { w e. ~P B | E. x ( w = C /\ ph ) } <-> ( ( E. x ph -> A e. B ) /\ A. x ( ph -> A e. C ) ) ) )