Theorem eqriv 2726

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqid  2729  cbvabv  2799  cbvabw  2800  cbvab  2801  vjust  3448  rabtru  3656  nfccdeq  3749  csbgfi  3882  difeqri  4091  uneqri  4119  ineqri  4175  symdifass  4225  indifdi  4257  undif3  4263  csbcom  4383  csbab  4403  pwpr  4865  pwtp  4866  pwv  4868  uniun  4894  int0  4926  intun  4944  iuncom  4963  iuncom4  4964  iunin2  5035  iinun2  5037  iundif2  5038  iunun  5057  iunxun  5058  iunxiun  5061  iinpw  5070  inuni  5305  unipw  5410  xpiundi  5709  xpiundir  5710  iunxpf  5812  cnvuni  5850  dmiun  5877  dmuni  5878  idinxpres  6018  rniun  6120  xpdifid  6141  cnvresima  6203  imaco  6224  rnco  6225  imaindm  6272  dfmpt3  6652  imaiun  7219  unon  7806  opabex3d  7944  opabex3rd  7945  opabex3  7946  fparlem1  8091  fparlem2  8092  oarec  8526  ecid  8753  qsid  8754  mapval2  8845  ixpin  8896  onfin2  9180  unfilem1  9254  unifpw  9306  dfom5  9603  alephsuc2  10033  ackbij2  10195  isf33lem  10319  dffin7-2  10351  fin1a2lem6  10358  acncc  10393  fin41  10397  iunfo  10492  grutsk  10775  grothac  10783  grothtsk  10788  dfz2  12548  qexALT  12923  dfrp2  13355  om2uzrani  13917  hashkf  14297  divalglem4  16366  1nprm  16649  nsgacs  19094  oppgsubm  19294  oppgsubg  19295  oppgcntz  19296  pmtrprfvalrn  19418  opprsubg  20261  opprunit  20286  opprirred  20331  opprsubrng  20468  opprsubrg  20502  00lss  20847  dfprm2  21383  unocv  21589  iunocv  21590  00ply1bas  22124  toprntopon  22812  unisngl  23414  zcld  24702  iundisj  25449  plyun0  26102  aannenlem2  26237  eqid1  30396  choc0  31255  chocnul  31257  spanunsni  31508  lncnbd  31967  adjbd1o  32014  rnbra  32036  pjimai  32105  iunin1f  32486  iundisjf  32518  xrdifh  32703  iundisjfi  32719  opprnsg  33455  ccfldextdgrr  33667  cmpcref  33840  eulerpartgbij  34363  eulerpartlemr  34365  oddprm2  34646  dfdm5  35760  dfrn5  35761  dffix2  35893  fixcnv  35896  dfom5b  35900  fnimage  35917  brimg  35925  bj-csbsnlem  36891  bj-projun  36982  bj-pw0ALT  37037  bj-vjust  37043  finxp1o  37380  iundif1  37588  poimirlem26  37640  csbcom2fi  38122  prtlem16  38862  sn-iotalem  42209  redvmptabs  42348  aaitgo  43151  imaiun1  43640  grumnueq  44276  nzss  44306  dfodd2  47637  dfeven5  47667  dfodd7  47668  ixpv  48878  isoval2  49024  oppcciceq  49041  oppczeroo  49226  dfinito4  49490  lmdfval2  49644  cmdfval2  49645  initocmd  49658  termolmd  49659