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 2604 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1717 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∈ wcel 1977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 |
This theorem is referenced by: eqid 2610 cbvab 2733 vjust 3174 nfccdeq 3400 difeqri 3692 uneqri 3717 incom 3767 ineqri 3768 symdifass 3815 indifdir 3842 undif3 3847 undif3OLD 3848 csbcom 3946 csbab 3960 pwpr 4368 pwtp 4369 pwv 4371 uniun 4392 int0 4425 intun 4444 intpr 4445 iuncom 4463 iuncom4 4464 iun0 4512 0iun 4513 iunin2 4520 iinun2 4522 iundif2 4523 iunun 4540 iunxun 4541 iunxiun 4544 iinpw 4550 inuni 4753 unipw 4845 xpiundi 5096 xpiundir 5097 0xp 5122 iunxpf 5192 cnvuni 5231 dmiun 5255 dmuni 5256 epini 5414 rniun 5462 xpdifid 5481 cnvresima 5541 imaco 5557 rnco 5558 dfmpt3 5927 imaiun 6407 snnex 6862 unon 6923 opabex3d 7037 opabex3 7038 fparlem1 7164 fparlem2 7165 oarec 7529 ecid 7699 qsid 7700 mapval2 7773 ixpin 7819 onfin2 8037 unfilem1 8109 unifpw 8152 dfom5 8430 alephsuc2 8786 ackbij2 8948 isf33lem 9071 dffin7-2 9103 fin1a2lem6 9110 acncc 9145 fin41 9149 iunfo 9240 grutsk 9523 grothac 9531 grothtsk 9536 dfz2 11272 qexALT 11679 om2uzrani 12613 hashkf 12981 divalglem4 14957 1nprm 15230 nsgacs 17453 oppgsubm 17615 oppgsubg 17616 oppgcntz 17617 pmtrprfvalrn 17731 opprsubg 18459 opprunit 18484 opprirred 18525 opprsubrg 18624 00lss 18763 00ply1bas 19431 dfprm2 19661 unocv 19843 iunocv 19844 unisngl 21140 zcld 22424 iundisj 23123 plyun0 23757 aannenlem2 23888 eqid1 26715 choc0 27569 chocnul 27571 spanunsni 27822 lncnbd 28281 adjbd1o 28328 rnbra 28350 pjimai 28419 rabtru 28723 iunin1f 28757 iundisjf 28784 dfrp2 28922 xrdifh 28932 iundisjfi 28942 cmpcref 29245 eulerpartgbij 29761 eulerpartlemr 29763 dfdm5 30921 dfrn5 30922 dffix2 31182 fixcnv 31185 dfom5b 31189 fnimage 31206 brimg 31214 bj-vjust 31974 bj-csbsnlem 32090 bj-projun 32175 bj-vjust2 32206 bj-toprntopon 32244 finxp0 32404 finxp1o 32405 iundif1 32553 poimirlem26 32605 csbcom2fi 33104 csbgfi 33105 prtlem16 33172 aaitgo 36751 imaiun1 36962 nzss 37538 dfodd2 40087 dfeven5 40116 dfodd7 40117 |
Copyright terms: Public domain | W3C validator |