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