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	⊢ ( 𝐴 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) }
	brfvopabrbr.2	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
	brfvopabrbr.3	⊢ Rel ( 𝐵 ‘ 𝑍 )
Assertion	brfvopabrbr	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		brfvopabrbr.1	⊢ ( 𝐴 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) }
2		brfvopabrbr.2	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
3		brfvopabrbr.3	⊢ Rel ( 𝐵 ‘ 𝑍 )
4		brne0	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → ( 𝐴 ‘ 𝑍 ) ≠ ∅ )
5		fvprc	⊢ ( ¬ 𝑍 ∈ V → ( 𝐴 ‘ 𝑍 ) = ∅ )
6	5	necon1ai	⊢ ( ( 𝐴 ‘ 𝑍 ) ≠ ∅ → 𝑍 ∈ V )
7	4 6	syl	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑍 ∈ V )
8	1	relopabi	⊢ Rel ( 𝐴 ‘ 𝑍 )
9	8	brrelex1i	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑋 ∈ V )
10	8	brrelex2i	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → 𝑌 ∈ V )
11	7 9 10	3jca	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
12		brne0	⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → ( 𝐵 ‘ 𝑍 ) ≠ ∅ )
13		fvprc	⊢ ( ¬ 𝑍 ∈ V → ( 𝐵 ‘ 𝑍 ) = ∅ )
14	13	necon1ai	⊢ ( ( 𝐵 ‘ 𝑍 ) ≠ ∅ → 𝑍 ∈ V )
15	12 14	syl	⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑍 ∈ V )
16	3	brrelex1i	⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑋 ∈ V )
17	3	brrelex2i	⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → 𝑌 ∈ V )
18	15 16 17	3jca	⊢ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
19	18	adantr	⊢ ( ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) → ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
20	1	a1i	⊢ ( 𝑍 ∈ V → ( 𝐴 ‘ 𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵 ‘ 𝑍 ) 𝑦 ∧ 𝜑 ) } )
21	20 2	rbropap	⊢ ( ( 𝑍 ∈ V ∧ 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) ) )
22	11 19 21	pm5.21nii	⊢ ( 𝑋 ( 𝐴 ‘ 𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵 ‘ 𝑍 ) 𝑌 ∧ 𝜓 ) )