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 5136 | . 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) |
5 | 1, 2, 4 | mp2an 704 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∈ wcel 1977 〈cop 4131 Rel wrel 5043 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-opab 4644 df-xp 5044 df-rel 5045 |
This theorem is referenced by: eqbrriv 5138 inopab 5174 difopab 5175 dfres2 5372 restidsing 5377 restidsingOLD 5378 cnvopab 5452 cnv0OLD 5455 cnvdif 5458 difxp 5477 cnvcnvsn 5530 dfco2 5551 coiun 5562 co02 5566 coass 5571 ressn 5588 ovoliunlem1 23077 h2hlm 27221 cnvco1 30903 cnvco2 30904 cnviun 36961 coiun1 36963 |
Copyright terms: Public domain | W3C validator |