Theorem eqriv 2734

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 2730	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		eqriv.1	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
3	1, 2	mpgbir 1801	1 ⊢ 𝐴 = 𝐵

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqid  2737  cbvabv  2807  cbvabw  2808  cbvab  2809  vjust  3431  rabtru  3633  nfccdeq  3725  csbgfi  3858  difeqri  4069  uneqri  4097  ineqri  4153  symdifass  4203  indifdi  4235  undif3  4241  csbcom  4361  csbab  4381  pwpr  4845  pwtp  4846  pwv  4848  uniun  4874  int0  4905  intun  4923  iuncom  4942  iuncom4  4943  iunin2  5014  iinun2  5016  iundif2  5017  iunun  5036  iunxun  5037  iunxiun  5040  iinpw  5049  inuni  5287  unipw  5397  xpiundi  5695  xpiundir  5696  iunxpf  5797  cnvuni  5835  dmiun  5862  dmuni  5863  idinxpres  6006  rniun  6105  xpdifid  6126  cnvresima  6188  imaco  6209  rnco  6210  rncoOLD  6211  imaindm  6257  dfmpt3  6626  imaiun  7193  unon  7775  opabex3d  7911  opabex3rd  7912  opabex3  7913  fparlem1  8055  fparlem2  8056  oarec  8490  ecid  8720  qsid  8721  mapval2  8813  ixpin  8864  onfin2  9144  unfilem1  9208  unifpw  9258  dfom5  9562  alephsuc2  9993  ackbij2  10155  isf33lem  10279  dffin7-2  10311  fin1a2lem6  10318  acncc  10353  fin41  10357  iunfo  10452  grutsk  10736  grothac  10744  grothtsk  10749  dfz2  12534  qexALT  12905  dfrp2  13338  om2uzrani  13905  hashkf  14285  divalglem4  16356  1nprm  16639  nsgacs  19128  oppgsubm  19328  oppgsubg  19329  oppgcntz  19330  pmtrprfvalrn  19454  opprsubg  20323  opprunit  20348  opprirred  20393  opprsubrng  20527  opprsubrg  20561  00lss  20927  dfprm2  21463  unocv  21670  iunocv  21671  00ply1bas  22213  toprntopon  22900  unisngl  23502  zcld  24789  iundisj  25525  plyun0  26172  aannenlem2  26306  dfz12s2  28494  eqid1  30552  choc0  31412  chocnul  31414  spanunsni  31665  lncnbd  32124  adjbd1o  32171  rnbra  32193  pjimai  32262  iunin1f  32642  iundisjf  32674  xrdifh  32868  iundisjfi  32884  opprnsg  33559  ccfldextdgrr  33832  cmpcref  34010  eulerpartgbij  34532  eulerpartlemr  34534  oddprm2  34815  dfdm5  35971  dfrn5  35972  dffix2  36101  fixcnv  36104  dfom5b  36108  fnimage  36125  brimg  36133  bj-csbsnlem  37226  bj-projun  37317  bj-pw0ALT  37372  bj-vjust  37378  finxp1o  37722  iundif1  37929  poimirlem26  37981  csbcom2fi  38463  dfsucmap3  38798  prtlem16  39329  sn-iotalem  42676  redvmptabs  42806  aaitgo  43608  imaiun1  44096  grumnueq  44732  nzss  44762  dfodd2  48124  dfeven5  48154  dfodd7  48155  ixpv  49377  isoval2  49522  oppcciceq  49539  oppczeroo  49724  dfinito4  49988  lmdfval2  50142  cmdfval2  50143  initocmd  50156  termolmd  50157