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

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