![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqrelriiv | Structured version Visualization version GIF version |
Description: Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.) |
Ref | Expression |
---|---|
eqreliiv.1 | ⊢ Rel 𝐴 |
eqreliiv.2 | ⊢ Rel 𝐵 |
eqreliiv.3 | ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵) |
Ref | Expression |
---|---|
eqrelriiv | ⊢ 𝐴 = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqreliiv.1 | . 2 ⊢ Rel 𝐴 | |
2 | eqreliiv.2 | . 2 ⊢ Rel 𝐵 | |
3 | eqreliiv.3 | . . 3 ⊢ (〈𝑥, 𝑦〉 ∈ 𝐴 ↔ 〈𝑥, 𝑦〉 ∈ 𝐵) | |
4 | 3 | eqrelriv 5802 | . 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) |
5 | 1, 2, 4 | mp2an 692 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 = wceq 1537 ∈ wcel 2106 〈cop 4637 Rel wrel 5694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-ss 3980 df-opab 5211 df-xp 5695 df-rel 5696 |
This theorem is referenced by: eqbrriv 5804 inopab 5842 difopab 5843 difopabOLD 5844 inxp 5845 dfres2 6061 restidsing 6073 cnvopab 6160 cnvopabOLD 6161 cnvdif 6166 difxp 6186 cnvcnvsn 6241 dfco2 6267 coiun 6278 co02 6282 coass 6287 ressn 6307 ovoliunlem1 25551 h2hlm 31009 cnvco1 35739 cnvco2 35740 inxprnres 38274 cnviun 43640 coiun1 43642 |
Copyright terms: Public domain | W3C validator |