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 syl6bi
 |-  ( 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 syl6bi
 |-  ( ( 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 ) )