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 \land φ)\}$
	brfvopabrbr.2	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow ψ)$
	brfvopabrbr.3	$⊢ Rel B (Z)$
Assertion	brfvopabrbr	$⊢ X A (Z) Y \leftrightarrow (X B (Z) Y \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		brfvopabrbr.1	$⊢ A (Z) = \{⟨x, y⟩ \| (x B (Z) y \land φ)\}$
2		brfvopabrbr.2	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow ψ)$
3		brfvopabrbr.3	$⊢ Rel B (Z)$
4		brne0	$⊢ X A (Z) Y \to A (Z) \neq \emptyset$
5		fvprc	$⊢ \neg Z \in V \to A (Z) = \emptyset$
6	5	necon1ai	$⊢ A (Z) \neq \emptyset \to Z \in V$
7	4 6	syl	$⊢ X A (Z) Y \to Z \in V$
8	1	relopabiv	$⊢ Rel A (Z)$
9	8	brrelex1i	$⊢ X A (Z) Y \to X \in V$
10	8	brrelex2i	$⊢ X A (Z) Y \to Y \in V$
11	7 9 10	3jca	$⊢ X A (Z) Y \to (Z \in V \land X \in V \land Y \in V)$
12		brne0	$⊢ X B (Z) Y \to B (Z) \neq \emptyset$
13		fvprc	$⊢ \neg Z \in V \to B (Z) = \emptyset$
14	13	necon1ai	$⊢ B (Z) \neq \emptyset \to Z \in V$
15	12 14	syl	$⊢ X B (Z) Y \to Z \in V$
16	3	brrelex1i	$⊢ X B (Z) Y \to X \in V$
17	3	brrelex2i	$⊢ X B (Z) Y \to Y \in V$
18	15 16 17	3jca	$⊢ X B (Z) Y \to (Z \in V \land X \in V \land Y \in V)$
19	18	adantr	$⊢ (X B (Z) Y \land ψ) \to (Z \in V \land X \in V \land Y \in V)$
20	1	a1i	$⊢ Z \in V \to A (Z) = \{⟨x, y⟩ \| (x B (Z) y \land φ)\}$
21	20 2	rbropap	$⊢ (Z \in V \land X \in V \land Y \in V) \to (X A (Z) Y \leftrightarrow (X B (Z) Y \land ψ))$
22	11 19 21	pm5.21nii	$⊢ X A (Z) Y \leftrightarrow (X B (Z) Y \land ψ)$

Metamath Proof Explorer

Theorem brfvopabrbr

Proof