Metamath Proof Explorer

Theorem cnvcnvintabd

Description: Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020)

Ref Expression
Hypothesis cnvcnvintabd.x 
|- ( ph -> E. x ps )
Assertion cnvcnvintabd 
|- ( ph -> `' `' |^| { x | ps } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ps ) } )

Proof

Step Hyp Ref Expression
1 cnvcnvintabd.x 
 |-  ( ph -> E. x ps )
2 cnvcnv 
 |-  `' `' x = ( x i^i ( _V X. _V ) )
3 2 eleq2i 
 |-  ( y e. `' `' x <-> y e. ( x i^i ( _V X. _V ) ) )
4 elin 
 |-  ( y e. ( x i^i ( _V X. _V ) ) <-> ( y e. x /\ y e. ( _V X. _V ) ) )
5 4 rbaib 
 |-  ( y e. ( _V X. _V ) -> ( y e. ( x i^i ( _V X. _V ) ) <-> y e. x ) )
6 3 5 bitrid 
 |-  ( y e. ( _V X. _V ) -> ( y e. `' `' x <-> y e. x ) )
7 6 bicomd 
 |-  ( y e. ( _V X. _V ) -> ( y e. x <-> y e. `' `' x ) )
8 7 imbi2d 
 |-  ( y e. ( _V X. _V ) -> ( ( ps -> y e. x ) <-> ( ps -> y e. `' `' x ) ) )
9 8 albidv 
 |-  ( y e. ( _V X. _V ) -> ( A. x ( ps -> y e. x ) <-> A. x ( ps -> y e. `' `' x ) ) )
10 9 pm5.32i 
 |-  ( ( y e. ( _V X. _V ) /\ A. x ( ps -> y e. x ) ) <-> ( y e. ( _V X. _V ) /\ A. x ( ps -> y e. `' `' x ) ) )
11 pm5.5 
 |-  ( E. x ps -> ( ( E. x ps -> y e. ( _V X. _V ) ) <-> y e. ( _V X. _V ) ) )
12 1 11 syl 
 |-  ( ph -> ( ( E. x ps -> y e. ( _V X. _V ) ) <-> y e. ( _V X. _V ) ) )
13 12 bicomd 
 |-  ( ph -> ( y e. ( _V X. _V ) <-> ( E. x ps -> y e. ( _V X. _V ) ) ) )
14 13 anbi1d 
 |-  ( ph -> ( ( y e. ( _V X. _V ) /\ A. x ( ps -> y e. `' `' x ) ) <-> ( ( E. x ps -> y e. ( _V X. _V ) ) /\ A. x ( ps -> y e. `' `' x ) ) ) )
15 10 14 bitrid 
 |-  ( ph -> ( ( y e. ( _V X. _V ) /\ A. x ( ps -> y e. x ) ) <-> ( ( E. x ps -> y e. ( _V X. _V ) ) /\ A. x ( ps -> y e. `' `' x ) ) ) )
16 elcnvcnvintab 
 |-  ( y e. `' `' |^| { x | ps } <-> ( y e. ( _V X. _V ) /\ A. x ( ps -> y e. x ) ) )
17 vex 
 |-  x e. _V
18 cnvexg 
 |-  ( x e. _V -> `' x e. _V )
19 cnvexg 
 |-  ( `' x e. _V -> `' `' x e. _V )
20 17 18 19 mp2b 
 |-  `' `' x e. _V
21 relcnv 
 |-  Rel `' `' x
22 df-rel 
 |-  ( Rel `' `' x <-> `' `' x C_ ( _V X. _V ) )
23 21 22 mpbi 
 |-  `' `' x C_ ( _V X. _V )
24 20 23 elmapintrab 
 |-  ( y e. _V -> ( y e. |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ps ) } <-> ( ( E. x ps -> y e. ( _V X. _V ) ) /\ A. x ( ps -> y e. `' `' x ) ) ) )
25 24 elv 
 |-  ( y e. |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ps ) } <-> ( ( E. x ps -> y e. ( _V X. _V ) ) /\ A. x ( ps -> y e. `' `' x ) ) )
26 15 16 25 3bitr4g 
 |-  ( ph -> ( y e. `' `' |^| { x | ps } <-> y e. |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ps ) } ) )
27 26 eqrdv 
 |-  ( ph -> `' `' |^| { x | ps } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ps ) } )