This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brab2ddw2

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Hypotheses brab2dd.1 ⊢ φ → R = x y | x ∈ C ∧ y ∈ D ∧ ψ
brab2ddw.2 ⊢ x = A → ψ ↔ θ
brab2ddw.3 ⊢ y = B → θ ↔ χ
brab2ddw2.4 ⊢ x = A → C = U
brab2ddw2.5 ⊢ y = B → D = V
Assertion brab2ddw2 ⊢ φ → A R B ↔ A ∈ U ∧ B ∈ V ∧ χ

Proof

Step Hyp Ref Expression
1 brab2dd.1 ⊢ φ → R = x y | x ∈ C ∧ y ∈ D ∧ ψ
2 brab2ddw.2 ⊢ x = A → ψ ↔ θ
3 brab2ddw.3 ⊢ y = B → θ ↔ χ
4 brab2ddw2.4 ⊢ x = A → C = U
5 brab2ddw2.5 ⊢ y = B → D = V
6 2 3 sylan9bb ⊢ x = A ∧ y = B → ψ ↔ χ
7 6 adantl ⊢ φ ∧ x = A ∧ y = B → ψ ↔ χ
8 id ⊢ x = A → x = A
9 8 4 eleq12d ⊢ x = A → x ∈ C ↔ A ∈ U
10 id ⊢ y = B → y = B
11 10 5 eleq12d ⊢ y = B → y ∈ D ↔ B ∈ V
12 9 11 bi2anan9 ⊢ x = A ∧ y = B → x ∈ C ∧ y ∈ D ↔ A ∈ U ∧ B ∈ V
13 12 adantl ⊢ φ ∧ x = A ∧ y = B → x ∈ C ∧ y ∈ D ↔ A ∈ U ∧ B ∈ V
14 1 7 13 brab2dd ⊢ φ → A R B ↔ A ∈ U ∧ B ∈ V ∧ χ