Theorem eqriv 2730

Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
eqriv.1	⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)

Assertion

Ref	Expression
eqriv	⊢ 𝐴 = 𝐵

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqriv

Step	Hyp	Ref	Expression
1		dfcleq 2726	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1800	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113

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 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  eqid  2733  cbvabv  2803  cbvabw  2804  cbvab  2805  vjust  3438  rabtru  3641  nfccdeq  3733  csbgfi  3866  difeqri  4077  uneqri  4105  ineqri  4161  symdifass  4211  indifdi  4243  undif3  4249  csbcom  4369  csbab  4389  pwpr  4852  pwtp  4853  pwv  4855  uniun  4881  int0  4912  intun  4930  iuncom  4949  iuncom4  4950  iunin2  5021  iinun2  5023  iundif2  5024  iunun  5043  iunxun  5044  iunxiun  5047  iinpw  5056  inuni  5290  unipw  5393  xpiundi  5690  xpiundir  5691  iunxpf  5792  cnvuni  5830  dmiun  5857  dmuni  5858  idinxpres  6000  rniun  6099  xpdifid  6120  cnvresima  6182  imaco  6203  rnco  6204  rncoOLD  6205  imaindm  6251  dfmpt3  6620  imaiun  7185  unon  7767  opabex3d  7903  opabex3rd  7904  opabex3  7905  fparlem1  8048  fparlem2  8049  oarec  8483  ecid  8710  qsid  8711  mapval2  8802  ixpin  8853  onfin2  9132  unfilem1  9196  unifpw  9246  dfom5  9547  alephsuc2  9978  ackbij2  10140  isf33lem  10264  dffin7-2  10296  fin1a2lem6  10303  acncc  10338  fin41  10342  iunfo  10437  grutsk  10720  grothac  10728  grothtsk  10733  dfz2  12494  qexALT  12864  dfrp2  13296  om2uzrani  13861  hashkf  14241  divalglem4  16309  1nprm  16592  nsgacs  19076  oppgsubm  19276  oppgsubg  19277  oppgcntz  19278  pmtrprfvalrn  19402  opprsubg  20272  opprunit  20297  opprirred  20342  opprsubrng  20476  opprsubrg  20510  00lss  20876  dfprm2  21412  unocv  21619  iunocv  21620  00ply1bas  22153  toprntopon  22841  unisngl  23443  zcld  24730  iundisj  25477  plyun0  26130  aannenlem2  26265  eqid1  30449  choc0  31308  chocnul  31310  spanunsni  31561  lncnbd  32020  adjbd1o  32067  rnbra  32089  pjimai  32158  iunin1f  32539  iundisjf  32571  xrdifh  32767  iundisjfi  32783  opprnsg  33456  ccfldextdgrr  33706  cmpcref  33884  eulerpartgbij  34406  eulerpartlemr  34408  oddprm2  34689  dfdm5  35838  dfrn5  35839  dffix2  35968  fixcnv  35971  dfom5b  35975  fnimage  35992  brimg  36000  bj-csbsnlem  36968  bj-projun  37059  bj-pw0ALT  37114  bj-vjust  37120  finxp1o  37457  iundif1  37655  poimirlem26  37707  csbcom2fi  38189  dfsucmap3  38497  prtlem16  38989  sn-iotalem  42340  redvmptabs  42479  aaitgo  43280  imaiun1  43769  grumnueq  44405  nzss  44435  dfodd2  47761  dfeven5  47791  dfodd7  47792  ixpv  49015  isoval2  49161  oppcciceq  49178  oppczeroo  49363  dfinito4  49627  lmdfval2  49781  cmdfval2  49782  initocmd  49795  termolmd  49796