| 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 5799 | . 2 ⊢ ((Rel 𝐴 ∧ Rel 𝐵) → 𝐴 = 𝐵) |
| 5 | 1, 2, 4 | mp2an 692 | 1 ⊢ 𝐴 = 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ∈ wcel 2108 〈cop 4632 Rel wrel 5690 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-opab 5206 df-xp 5691 df-rel 5692 |
| This theorem is referenced by: eqbrriv 5801 inopab 5839 difopab 5840 difopabOLD 5841 inxp 5842 dfres2 6059 restidsing 6071 cnvopab 6157 cnvopabOLD 6158 cnvdif 6163 difxp 6184 cnvcnvsn 6239 dfco2 6265 coiun 6276 co02 6280 coass 6285 ressn 6305 ovoliunlem1 25537 h2hlm 30999 cnvco1 35759 cnvco2 35760 inxprnres 38293 cnviun 43663 coiun1 43665 coxp 48744 |
| Copyright terms: Public domain | W3C validator |