# 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}\left({Z}\right)=\left\{⟨{x},{y}⟩|\left({x}{B}\left({Z}\right){y}\wedge {\phi }\right)\right\}$
brfvopabrbr.2 ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to \left({\phi }↔{\psi }\right)$
brfvopabrbr.3 ${⊢}\mathrm{Rel}{B}\left({Z}\right)$
Assertion brfvopabrbr ${⊢}{X}{A}\left({Z}\right){Y}↔\left({X}{B}\left({Z}\right){Y}\wedge {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 brfvopabrbr.1 ${⊢}{A}\left({Z}\right)=\left\{⟨{x},{y}⟩|\left({x}{B}\left({Z}\right){y}\wedge {\phi }\right)\right\}$
2 brfvopabrbr.2 ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to \left({\phi }↔{\psi }\right)$
3 brfvopabrbr.3 ${⊢}\mathrm{Rel}{B}\left({Z}\right)$
4 brne0 ${⊢}{X}{A}\left({Z}\right){Y}\to {A}\left({Z}\right)\ne \varnothing$
5 fvprc ${⊢}¬{Z}\in \mathrm{V}\to {A}\left({Z}\right)=\varnothing$
6 5 necon1ai ${⊢}{A}\left({Z}\right)\ne \varnothing \to {Z}\in \mathrm{V}$
7 4 6 syl ${⊢}{X}{A}\left({Z}\right){Y}\to {Z}\in \mathrm{V}$
8 1 relopabi ${⊢}\mathrm{Rel}{A}\left({Z}\right)$
9 8 brrelex1i ${⊢}{X}{A}\left({Z}\right){Y}\to {X}\in \mathrm{V}$
10 8 brrelex2i ${⊢}{X}{A}\left({Z}\right){Y}\to {Y}\in \mathrm{V}$
11 7 9 10 3jca ${⊢}{X}{A}\left({Z}\right){Y}\to \left({Z}\in \mathrm{V}\wedge {X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$
12 brne0 ${⊢}{X}{B}\left({Z}\right){Y}\to {B}\left({Z}\right)\ne \varnothing$
13 fvprc ${⊢}¬{Z}\in \mathrm{V}\to {B}\left({Z}\right)=\varnothing$
14 13 necon1ai ${⊢}{B}\left({Z}\right)\ne \varnothing \to {Z}\in \mathrm{V}$
15 12 14 syl ${⊢}{X}{B}\left({Z}\right){Y}\to {Z}\in \mathrm{V}$
16 3 brrelex1i ${⊢}{X}{B}\left({Z}\right){Y}\to {X}\in \mathrm{V}$
17 3 brrelex2i ${⊢}{X}{B}\left({Z}\right){Y}\to {Y}\in \mathrm{V}$
18 15 16 17 3jca ${⊢}{X}{B}\left({Z}\right){Y}\to \left({Z}\in \mathrm{V}\wedge {X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$
19 18 adantr ${⊢}\left({X}{B}\left({Z}\right){Y}\wedge {\psi }\right)\to \left({Z}\in \mathrm{V}\wedge {X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)$
20 1 a1i ${⊢}{Z}\in \mathrm{V}\to {A}\left({Z}\right)=\left\{⟨{x},{y}⟩|\left({x}{B}\left({Z}\right){y}\wedge {\phi }\right)\right\}$
21 20 2 rbropap ${⊢}\left({Z}\in \mathrm{V}\wedge {X}\in \mathrm{V}\wedge {Y}\in \mathrm{V}\right)\to \left({X}{A}\left({Z}\right){Y}↔\left({X}{B}\left({Z}\right){Y}\wedge {\psi }\right)\right)$
22 11 19 21 pm5.21nii ${⊢}{X}{A}\left({Z}\right){Y}↔\left({X}{B}\left({Z}\right){Y}\wedge {\psi }\right)$