Metamath Proof Explorer


Theorem eqbrriv

Description: Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006)

Ref Expression
Hypotheses eqbrriv.1 Rel 𝐴
eqbrriv.2 Rel 𝐵
eqbrriv.3 ( 𝑥 𝐴 𝑦𝑥 𝐵 𝑦 )
Assertion eqbrriv 𝐴 = 𝐵

Proof

Step Hyp Ref Expression
1 eqbrriv.1 Rel 𝐴
2 eqbrriv.2 Rel 𝐵
3 eqbrriv.3 ( 𝑥 𝐴 𝑦𝑥 𝐵 𝑦 )
4 df-br ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
5 df-br ( 𝑥 𝐵 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
6 3 4 5 3bitr3i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 )
7 1 2 6 eqrelriiv 𝐴 = 𝐵