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 2815 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1800 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1537 ∈ wcel 2114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 |
This theorem is referenced by: eqid 2821 cbvabv 2889 cbvabw 2890 cbvab 2891 vjust 3495 rabtru 3677 nfccdeq 3769 csbgfi 3903 difeqri 4101 uneqri 4127 incomOLD 4179 ineqri 4180 symdifass 4228 indifdir 4260 undif3 4265 csbcom 4369 csbab 4389 pwpr 4832 pwtp 4833 pwv 4835 uniun 4861 int0 4890 intun 4908 intpr 4909 iuncom 4926 iuncom4 4927 iunin2 4993 iinun2 4995 iundif2 4996 iunun 5015 iunxun 5016 iunxiun 5019 iinpw 5028 inuni 5246 unipw 5343 xpiundi 5622 xpiundir 5623 iunxpf 5719 cnvuni 5757 dmiun 5782 dmuni 5783 idinxpres 5914 epini 5959 rniun 6006 xpdifid 6025 cnvresima 6087 imaco 6104 rnco 6105 dfmpt3 6482 imaiun 7004 unon 7546 opabex3d 7666 opabex3rd 7667 opabex3 7668 fparlem1 7807 fparlem2 7808 oarec 8188 ecid 8362 qsid 8363 mapval2 8436 ixpin 8487 onfin2 8710 unfilem1 8782 unifpw 8827 dfom5 9113 alephsuc2 9506 ackbij2 9665 isf33lem 9788 dffin7-2 9820 fin1a2lem6 9827 acncc 9862 fin41 9866 iunfo 9961 grutsk 10244 grothac 10252 grothtsk 10257 dfz2 12001 qexALT 12364 om2uzrani 13321 hashkf 13693 divalglem4 15747 1nprm 16023 nsgacs 18314 oppgsubm 18490 oppgsubg 18491 oppgcntz 18492 pmtrprfvalrn 18616 opprsubg 19386 opprunit 19411 opprirred 19452 opprsubrg 19556 00lss 19713 00ply1bas 20408 dfprm2 20641 unocv 20824 iunocv 20825 toprntopon 21533 unisngl 22135 zcld 23421 iundisj 24149 plyun0 24787 aannenlem2 24918 eqid1 28246 choc0 29103 chocnul 29105 spanunsni 29356 lncnbd 29815 adjbd1o 29862 rnbra 29884 pjimai 29953 iunin1f 30309 iundisjf 30339 dfrp2 30491 xrdifh 30503 iundisjfi 30519 ccfldextdgrr 31057 cmpcref 31114 eulerpartgbij 31630 eulerpartlemr 31632 oddprm2 31926 dfdm5 33016 dfrn5 33017 imaindm 33022 dffix2 33366 fixcnv 33369 dfom5b 33373 fnimage 33390 brimg 33398 bj-csbsnlem 34223 bj-projun 34309 bj-pw0ALT 34345 bj-vjust 34349 finxp1o 34676 wl-dfrabv 34877 iundif1 34881 poimirlem26 34933 csbcom2fi 35421 prtlem16 36020 aaitgo 39782 imaiun1 40016 grumnueq 40643 nzss 40669 dfodd2 43821 dfeven5 43851 dfodd7 43852 |
Copyright terms: Public domain | W3C validator |