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 | ⊢ 𝐴 = 𝐵 |
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 | ⊢ 𝐴 = 𝐵 |