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 ( 𝐴𝑍 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ( 𝐵𝑍 ) 𝑦𝜑 ) }
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 relopabiv 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 ( 𝑋 ( 𝐴𝑍 ) 𝑌 ↔ ( 𝑋 ( 𝐵𝑍 ) 𝑌𝜓 ) )