![]() |
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 2726 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1802 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 ∈ wcel 2107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 |
This theorem is referenced by: eqid 2733 cbvabv 2806 cbvabw 2807 cbvabwOLD 2808 cbvab 2809 vjust 3476 rabtru 3679 nfccdeq 3773 csbgfi 3913 difeqri 4123 uneqri 4150 ineqri 4203 symdifass 4250 indifdi 4282 indifdirOLD 4284 undif3 4289 csbcom 4416 csbab 4436 pwpr 4901 pwtp 4902 pwv 4904 uniun 4933 int0 4965 intun 4983 intprOLD 4986 iuncom 5003 iuncom4 5004 iunin2 5073 iinun2 5075 iundif2 5076 iunun 5095 iunxun 5096 iunxiun 5099 iinpw 5108 inuni 5342 unipw 5449 xpiundi 5744 xpiundir 5745 iunxpf 5846 cnvuni 5884 dmiun 5911 dmuni 5912 idinxpres 6044 rniun 6144 xpdifid 6164 cnvresima 6226 imaco 6247 rnco 6248 imaindm 6295 dfmpt3 6681 imaiun 7239 unon 7814 opabex3d 7947 opabex3rd 7948 opabex3 7949 fparlem1 8093 fparlem2 8094 oarec 8558 ecid 8772 qsid 8773 mapval2 8862 ixpin 8913 onfin2 9227 unfilem1 9306 unifpw 9351 dfom5 9641 alephsuc2 10071 ackbij2 10234 isf33lem 10357 dffin7-2 10389 fin1a2lem6 10396 acncc 10431 fin41 10435 iunfo 10530 grutsk 10813 grothac 10821 grothtsk 10826 dfz2 12573 qexALT 12944 dfrp2 13369 om2uzrani 13913 hashkf 14288 divalglem4 16335 1nprm 16612 nsgacs 19036 oppgsubm 19222 oppgsubg 19223 oppgcntz 19224 pmtrprfvalrn 19349 opprsubg 20155 opprunit 20180 opprirred 20225 opprsubrg 20372 00lss 20540 dfprm2 21027 unocv 21217 iunocv 21218 00ply1bas 21744 toprntopon 22409 unisngl 23013 zcld 24311 iundisj 25047 plyun0 25693 aannenlem2 25824 eqid1 29700 choc0 30557 chocnul 30559 spanunsni 30810 lncnbd 31269 adjbd1o 31316 rnbra 31338 pjimai 31407 iunin1f 31767 iundisjf 31798 xrdifh 31969 iundisjfi 31985 opprnsg 32551 ccfldextdgrr 32691 cmpcref 32768 eulerpartgbij 33309 eulerpartlemr 33311 oddprm2 33605 dfdm5 34682 dfrn5 34683 dffix2 34815 fixcnv 34818 dfom5b 34822 fnimage 34839 brimg 34847 bj-csbsnlem 35721 bj-projun 35813 bj-pw0ALT 35868 bj-vjust 35874 finxp1o 36211 iundif1 36400 poimirlem26 36452 csbcom2fi 36934 prtlem16 37677 sn-iotalem 40986 aaitgo 41837 imaiun1 42335 grumnueq 42979 nzss 43009 dfodd2 46239 dfeven5 46269 dfodd7 46270 opprsubrng 46671 |
Copyright terms: Public domain | W3C validator |