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 ∧ φ
brfvopabrbr.2 ⊢ x = X ∧ y = Y → φ ↔ ψ
brfvopabrbr.3 ⊢ Rel ⁡ B ⁡ Z
Assertion brfvopabrbr ⊢ X A ⁡ Z Y ↔ X B ⁡ Z Y ∧ ψ

Proof

Step Hyp Ref Expression
1 brfvopabrbr.1 ⊢ A ⁡ Z = x y | x B ⁡ Z y ∧ φ
2 brfvopabrbr.2 ⊢ x = X ∧ y = Y → φ ↔ ψ
3 brfvopabrbr.3 ⊢ Rel ⁡ B ⁡ Z
4 brne0 ⊢ X A ⁡ Z Y → A ⁡ Z ≠ ∅
5 fvprc ⊢ ¬ Z ∈ V → A ⁡ Z = ∅
6 5 necon1ai ⊢ A ⁡ Z ≠ ∅ → Z ∈ V
7 4 6 syl ⊢ X A ⁡ Z Y → Z ∈ V
8 1 relopabiv ⊢ Rel ⁡ A ⁡ Z
9 8 brrelex1i ⊢ X A ⁡ Z Y → X ∈ V
10 8 brrelex2i ⊢ X A ⁡ Z Y → Y ∈ V
11 7 9 10 3jca ⊢ X A ⁡ Z Y → Z ∈ V ∧ X ∈ V ∧ Y ∈ V
12 brne0 ⊢ X B ⁡ Z Y → B ⁡ Z ≠ ∅
13 fvprc ⊢ ¬ Z ∈ V → B ⁡ Z = ∅
14 13 necon1ai ⊢ B ⁡ Z ≠ ∅ → Z ∈ V
15 12 14 syl ⊢ X B ⁡ Z Y → Z ∈ V
16 3 brrelex1i ⊢ X B ⁡ Z Y → X ∈ V
17 3 brrelex2i ⊢ X B ⁡ Z Y → Y ∈ V
18 15 16 17 3jca ⊢ X B ⁡ Z Y → Z ∈ V ∧ X ∈ V ∧ Y ∈ V
19 18 adantr ⊢ X B ⁡ Z Y ∧ ψ → Z ∈ V ∧ X ∈ V ∧ Y ∈ V
20 1 a1i ⊢ Z ∈ V → A ⁡ Z = x y | x B ⁡ Z y ∧ φ
21 20 2 rbropap ⊢ Z ∈ V ∧ X ∈ V ∧ Y ∈ V → X A ⁡ Z Y ↔ X B ⁡ Z Y ∧ ψ
22 11 19 21 pm5.21nii ⊢ X A ⁡ Z Y ↔ X B ⁡ Z Y ∧ ψ