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

Metamath Proof Explorer

Theorem brfvopab

Description: The classes involved in a binary relation of a function value which is an ordered-pair class abstraction are sets. (Contributed by AV, 7-Jan-2021)

Ref Expression
Hypothesis brfvopab.1 
|- ( X e. _V -> ( F ` X ) = { <. y , z >. | ph } )
Assertion brfvopab 
|- ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) )

Proof

Step Hyp Ref Expression
1 brfvopab.1 
 |-  ( X e. _V -> ( F ` X ) = { <. y , z >. | ph } )
2 1 breqd 
 |-  ( X e. _V -> ( A ( F ` X ) B <-> A { <. y , z >. | ph } B ) )
3 brabv 
 |-  ( A { <. y , z >. | ph } B -> ( A e. _V /\ B e. _V ) )
4 2 3 biimtrdi 
 |-  ( X e. _V -> ( A ( F ` X ) B -> ( A e. _V /\ B e. _V ) ) )
5 4 imdistani 
 |-  ( ( X e. _V /\ A ( F ` X ) B ) -> ( X e. _V /\ ( A e. _V /\ B e. _V ) ) )
6 3anass 
 |-  ( ( X e. _V /\ A e. _V /\ B e. _V ) <-> ( X e. _V /\ ( A e. _V /\ B e. _V ) ) )
7 5 6 sylibr 
 |-  ( ( X e. _V /\ A ( F ` X ) B ) -> ( X e. _V /\ A e. _V /\ B e. _V ) )
8 7 ex 
 |-  ( X e. _V -> ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) )
9 fvprc 
 |-  ( -. X e. _V -> ( F ` X ) = (/) )
10 breq 
 |-  ( ( F ` X ) = (/) -> ( A ( F ` X ) B <-> A (/) B ) )
11 br0 
 |-  -. A (/) B
12 11 pm2.21i 
 |-  ( A (/) B -> ( X e. _V /\ A e. _V /\ B e. _V ) )
13 10 12 biimtrdi 
 |-  ( ( F ` X ) = (/) -> ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) )
14 9 13 syl 
 |-  ( -. X e. _V -> ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) ) )
15 8 14 pm2.61i 
 |-  ( A ( F ` X ) B -> ( X e. _V /\ A e. _V /\ B e. _V ) )