Metamath Proof Explorer


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