| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqriv | Structured version Visualization version GIF version | ||
| Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.) |
| Ref | Expression |
|---|---|
| eqriv.1 | ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) |
| Ref | Expression |
|---|---|
| eqriv | ⊢ 𝐴 = 𝐵 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfcleq 2730 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
| 2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
| 3 | 1, 2 | mpgbir 1799 | 1 ⊢ 𝐴 = 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 = wceq 1540 ∈ wcel 2108 |
| 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-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 |
| This theorem is referenced by: eqid 2737 cbvabv 2812 cbvabw 2813 cbvab 2814 vjust 3481 rabtru 3689 nfccdeq 3784 csbgfi 3919 difeqri 4128 uneqri 4156 ineqri 4212 symdifass 4262 indifdi 4294 undif3 4300 csbcom 4420 csbab 4440 pwpr 4901 pwtp 4902 pwv 4904 uniun 4930 int0 4962 intun 4980 iuncom 4999 iuncom4 5000 iunin2 5071 iinun2 5073 iundif2 5074 iunun 5093 iunxun 5094 iunxiun 5097 iinpw 5106 inuni 5350 unipw 5455 xpiundi 5756 xpiundir 5757 iunxpf 5859 cnvuni 5897 dmiun 5924 dmuni 5925 idinxpres 6065 rniun 6167 xpdifid 6188 cnvresima 6250 imaco 6271 rnco 6272 imaindm 6319 dfmpt3 6702 imaiun 7265 unon 7851 opabex3d 7990 opabex3rd 7991 opabex3 7992 fparlem1 8137 fparlem2 8138 oarec 8600 ecid 8822 qsid 8823 mapval2 8912 ixpin 8963 onfin2 9268 unfilem1 9343 unifpw 9395 dfom5 9690 alephsuc2 10120 ackbij2 10282 isf33lem 10406 dffin7-2 10438 fin1a2lem6 10445 acncc 10480 fin41 10484 iunfo 10579 grutsk 10862 grothac 10870 grothtsk 10875 dfz2 12632 qexALT 13006 dfrp2 13436 om2uzrani 13993 hashkf 14371 divalglem4 16433 1nprm 16716 nsgacs 19180 oppgsubm 19381 oppgsubg 19382 oppgcntz 19383 pmtrprfvalrn 19506 opprsubg 20352 opprunit 20377 opprirred 20422 opprsubrng 20559 opprsubrg 20593 00lss 20939 dfprm2 21484 unocv 21698 iunocv 21699 00ply1bas 22241 toprntopon 22931 unisngl 23535 zcld 24835 iundisj 25583 plyun0 26236 aannenlem2 26371 eqid1 30486 choc0 31345 chocnul 31347 spanunsni 31598 lncnbd 32057 adjbd1o 32104 rnbra 32126 pjimai 32195 iunin1f 32570 iundisjf 32602 xrdifh 32782 iundisjfi 32798 opprnsg 33512 ccfldextdgrr 33722 cmpcref 33849 eulerpartgbij 34374 eulerpartlemr 34376 oddprm2 34670 dfdm5 35773 dfrn5 35774 dffix2 35906 fixcnv 35909 dfom5b 35913 fnimage 35930 brimg 35938 bj-csbsnlem 36904 bj-projun 36995 bj-pw0ALT 37050 bj-vjust 37056 finxp1o 37393 iundif1 37601 poimirlem26 37653 csbcom2fi 38135 prtlem16 38870 sn-iotalem 42260 redvmptabs 42390 aaitgo 43174 imaiun1 43664 grumnueq 44306 nzss 44336 dfodd2 47623 dfeven5 47653 dfodd7 47654 |
| Copyright terms: Public domain | W3C validator |