Metamath Proof Explorer

Theorem relintab

Description: Value of the intersection of a class when it is a relation. (Contributed by RP, 12-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 cnvcnv 
 |-  `' `' |^| { x | ph } = ( |^| { x | ph } i^i ( _V X. _V ) )
2 incom 
 |-  ( |^| { x | ph } i^i ( _V X. _V ) ) = ( ( _V X. _V ) i^i |^| { x | ph } )
3 1 2 eqtri 
 |-  `' `' |^| { x | ph } = ( ( _V X. _V ) i^i |^| { x | ph } )
4 dfrel2 
 |-  ( Rel |^| { x | ph } <-> `' `' |^| { x | ph } = |^| { x | ph } )
5 4 biimpi 
 |-  ( Rel |^| { x | ph } -> `' `' |^| { x | ph } = |^| { x | ph } )
6 relintabex 
 |-  ( Rel |^| { x | ph } -> E. x ph )
7 6 xpinintabd 
 |-  ( Rel |^| { x | ph } -> ( ( _V X. _V ) i^i |^| { x | ph } ) = |^| { w e. ~P ( _V X. _V ) | E. x ( w = ( ( _V X. _V ) i^i x ) /\ ph ) } )
8 incom 
 |-  ( ( _V X. _V ) i^i x ) = ( x i^i ( _V X. _V ) )
9 cnvcnv 
 |-  `' `' x = ( x i^i ( _V X. _V ) )
10 8 9 eqtr4i 
 |-  ( ( _V X. _V ) i^i x ) = `' `' x
11 10 eqeq2i 
 |-  ( w = ( ( _V X. _V ) i^i x ) <-> w = `' `' x )
12 11 anbi1i 
 |-  ( ( w = ( ( _V X. _V ) i^i x ) /\ ph ) <-> ( w = `' `' x /\ ph ) )
13 12 exbii 
 |-  ( E. x ( w = ( ( _V X. _V ) i^i x ) /\ ph ) <-> E. x ( w = `' `' x /\ ph ) )
14 13 rabbii 
 |-  { w e. ~P ( _V X. _V ) | E. x ( w = ( ( _V X. _V ) i^i x ) /\ ph ) } = { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ph ) }
15 14 inteqi 
 |-  |^| { w e. ~P ( _V X. _V ) | E. x ( w = ( ( _V X. _V ) i^i x ) /\ ph ) } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ph ) }
16 7 15 eqtrdi 
 |-  ( Rel |^| { x | ph } -> ( ( _V X. _V ) i^i |^| { x | ph } ) = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ph ) } )
17 3 5 16 3eqtr3a 
 |-  ( Rel |^| { x | ph } -> |^| { x | ph } = |^| { w e. ~P ( _V X. _V ) | E. x ( w = `' `' x /\ ph ) } )