Theorem eqbrrdv

Description: Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	eqbrrdv.1	⊢ ( 𝜑 → Rel 𝐴 )
	eqbrrdv.2	⊢ ( 𝜑 → Rel 𝐵 )
	eqbrrdv.3	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
Assertion	eqbrrdv	⊢ ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqbrrdv.1	⊢ ( 𝜑 → Rel 𝐴 )
2		eqbrrdv.2	⊢ ( 𝜑 → Rel 𝐵 )
3		eqbrrdv.3	⊢ ( 𝜑 → ( 𝑥 𝐴 𝑦 ↔ 𝑥 𝐵 𝑦 ) )
4		df-br	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
5		df-br	⊢ ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
6	3 4 5	3bitr3g	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
7	6	alrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
8		eqrel	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
10	7 9	mpbird	⊢ ( 𝜑 → 𝐴 = 𝐵 )