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	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝜒 ) ) )