Theorem brfvopabrbr

Description: The binary relation of a function value which is an ordered-pair class abstraction of a restricted binary relation is the restricted binary relation. The first hypothesis can often be obtained by using fvmptopab . (Contributed by AV, 29-Oct-2021)

	Ref	Expression
Hypotheses	brfvopabrbr.1	|- ( A ` Z ) = { <. x , y >. | ( x ( B ` Z ) y /\ ph ) }
	brfvopabrbr.2	|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
	brfvopabrbr.3	|- Rel ( B ` Z )
Assertion	brfvopabrbr	|- ( X ( A ` Z ) Y <-> ( X ( B ` Z ) Y /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		brfvopabrbr.1	|- ( A ` Z ) = { <. x , y >. | ( x ( B ` Z ) y /\ ph ) }
2		brfvopabrbr.2	|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
3		brfvopabrbr.3	|- Rel ( B ` Z )
4		brne0	|- ( X ( A ` Z ) Y -> ( A ` Z ) =/= (/) )
5		fvprc	|- ( -. Z e. _V -> ( A ` Z ) = (/) )
6	5	necon1ai	|- ( ( A ` Z ) =/= (/) -> Z e. _V )
7	4 6	syl	|- ( X ( A ` Z ) Y -> Z e. _V )
8	1	relopabiv	|- Rel ( A ` Z )
9	8	brrelex1i	|- ( X ( A ` Z ) Y -> X e. _V )
10	8	brrelex2i	|- ( X ( A ` Z ) Y -> Y e. _V )
11	7 9 10	3jca	|- ( X ( A ` Z ) Y -> ( Z e. _V /\ X e. _V /\ Y e. _V ) )
12		brne0	|- ( X ( B ` Z ) Y -> ( B ` Z ) =/= (/) )
13		fvprc	|- ( -. Z e. _V -> ( B ` Z ) = (/) )
14	13	necon1ai	|- ( ( B ` Z ) =/= (/) -> Z e. _V )
15	12 14	syl	|- ( X ( B ` Z ) Y -> Z e. _V )
16	3	brrelex1i	|- ( X ( B ` Z ) Y -> X e. _V )
17	3	brrelex2i	|- ( X ( B ` Z ) Y -> Y e. _V )
18	15 16 17	3jca	|- ( X ( B ` Z ) Y -> ( Z e. _V /\ X e. _V /\ Y e. _V ) )
19	18	adantr	|- ( ( X ( B ` Z ) Y /\ ps ) -> ( Z e. _V /\ X e. _V /\ Y e. _V ) )
20	1	a1i	|- ( Z e. _V -> ( A ` Z ) = { <. x , y >. | ( x ( B ` Z ) y /\ ph ) } )
21	20 2	rbropap	|- ( ( Z e. _V /\ X e. _V /\ Y e. _V ) -> ( X ( A ` Z ) Y <-> ( X ( B ` Z ) Y /\ ps ) ) )
22	11 19 21	pm5.21nii	|- ( X ( A ` Z ) Y <-> ( X ( B ` Z ) Y /\ ps ) )