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

Metamath Proof Explorer

Theorem brab2dd

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 ⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } )
brab2dd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
brab2dd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) )
Assertion brab2dd ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )

Proof

Step Hyp Ref Expression
1 brab2dd.1 ⊢ ( 𝜑 → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } )
2 brab2dd.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( 𝜓 ↔ 𝜒 ) )
3 brab2dd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) )
4 df-br ⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
5 1 eleq2d ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } ) )
6 4 5 bitrid ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } ) )
7 elopab ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) )
8 6 7 bitrdi ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ) )
9 simpl ⊢ ( ( 𝜑 ∧ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ) → 𝜑 )
10 eqcom ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
11 vex ⊢ 𝑥 ∈ V
12 vex ⊢ 𝑦 ∈ V
13 11 12 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
14 10 13 sylbb1 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
15 14 ad2antrl ⊢ ( ( 𝜑 ∧ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ) → ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
16 simprrl ⊢ ( ( 𝜑 ∧ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ) → ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) )
17 3 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) )
18 9 15 16 17 syl21anc ⊢ ( ( 𝜑 ∧ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) )
19 18 ex ⊢ ( 𝜑 → ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) )
20 19 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) )
21 20 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) )
22 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) )
23 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑈 )
24 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
25 3 2 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )
26 25 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )
27 23 24 26 copsex2dv ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )
28 21 22 27 bibiad ⊢ ( 𝜑 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝜓 ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )
29 8 28 bitrd ⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )