This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fliftel

Description: Elementhood in the relation F . (Contributed by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypotheses flift.1 
|- F = ran ( x e. X |-> <. A , B >. )
flift.2 
|- ( ( ph /\ x e. X ) -> A e. R )
flift.3 
|- ( ( ph /\ x e. X ) -> B e. S )
Assertion fliftel 
|- ( ph -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )

Proof

Step Hyp Ref Expression
1 flift.1 
 |-  F = ran ( x e. X |-> <. A , B >. )
2 flift.2 
 |-  ( ( ph /\ x e. X ) -> A e. R )
3 flift.3 
 |-  ( ( ph /\ x e. X ) -> B e. S )
4 df-br 
 |-  ( C F D <-> <. C , D >. e. F )
5 1 eleq2i 
 |-  ( <. C , D >. e. F <-> <. C , D >. e. ran ( x e. X |-> <. A , B >. ) )
6 eqid 
 |-  ( x e. X |-> <. A , B >. ) = ( x e. X |-> <. A , B >. )
7 opex 
 |-  <. A , B >. e. _V
8 6 7 elrnmpti 
 |-  ( <. C , D >. e. ran ( x e. X |-> <. A , B >. ) <-> E. x e. X <. C , D >. = <. A , B >. )
9 4 5 8 3bitri 
 |-  ( C F D <-> E. x e. X <. C , D >. = <. A , B >. )
10 opthg2 
 |-  ( ( A e. R /\ B e. S ) -> ( <. C , D >. = <. A , B >. <-> ( C = A /\ D = B ) ) )
11 2 3 10 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( <. C , D >. = <. A , B >. <-> ( C = A /\ D = B ) ) )
12 11 rexbidva 
 |-  ( ph -> ( E. x e. X <. C , D >. = <. A , B >. <-> E. x e. X ( C = A /\ D = B ) ) )
13 9 12 bitrid 
 |-  ( ph -> ( C F D <-> E. x e. X ( C = A /\ D = B ) ) )