Theorem eqriv 2733

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 2729	. 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 2708

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

This theorem is referenced by:  eqid  2736  cbvabv  2806  cbvabw  2807  cbvab  2808  vjust  3441  rabtru  3644  nfccdeq  3736  csbgfi  3869  difeqri  4080  uneqri  4108  ineqri  4164  symdifass  4214  indifdi  4246  undif3  4252  csbcom  4372  csbab  4392  pwpr  4857  pwtp  4858  pwv  4860  uniun  4886  int0  4917  intun  4935  iuncom  4954  iuncom4  4955  iunin2  5026  iinun2  5028  iundif2  5029  iunun  5048  iunxun  5049  iunxiun  5052  iinpw  5061  inuni  5295  unipw  5398  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  7191  unon  7773  opabex3d  7909  opabex3rd  7910  opabex3  7911  fparlem1  8054  fparlem2  8055  oarec  8489  ecid  8717  qsid  8718  mapval2  8810  ixpin  8861  onfin2  9141  unfilem1  9205  unifpw  9255  dfom5  9559  alephsuc2  9990  ackbij2  10152  isf33lem  10276  dffin7-2  10308  fin1a2lem6  10315  acncc  10350  fin41  10354  iunfo  10449  grutsk  10733  grothac  10741  grothtsk  10746  dfz2  12507  qexALT  12877  dfrp2  13310  om2uzrani  13875  hashkf  14255  divalglem4  16323  1nprm  16606  nsgacs  19091  oppgsubm  19291  oppgsubg  19292  oppgcntz  19293  pmtrprfvalrn  19417  opprsubg  20288  opprunit  20313  opprirred  20358  opprsubrng  20492  opprsubrg  20526  00lss  20892  dfprm2  21428  unocv  21635  iunocv  21636  00ply1bas  22180  toprntopon  22869  unisngl  23471  zcld  24758  iundisj  25505  plyun0  26158  aannenlem2  26293  dfz12s2  28484  eqid1  30542  choc0  31401  chocnul  31403  spanunsni  31654  lncnbd  32113  adjbd1o  32160  rnbra  32182  pjimai  32251  iunin1f  32632  iundisjf  32664  xrdifh  32860  iundisjfi  32876  opprnsg  33565  ccfldextdgrr  33829  cmpcref  34007  eulerpartgbij  34529  eulerpartlemr  34531  oddprm2  34812  dfdm5  35967  dfrn5  35968  dffix2  36097  fixcnv  36100  dfom5b  36104  fnimage  36121  brimg  36129  bj-csbsnlem  37104  bj-projun  37195  bj-pw0ALT  37250  bj-vjust  37256  finxp1o  37593  iundif1  37791  poimirlem26  37843  csbcom2fi  38325  dfsucmap3  38633  prtlem16  39125  sn-iotalem  42473  redvmptabs  42611  aaitgo  43400  imaiun1  43888  grumnueq  44524  nzss  44554  dfodd2  47878  dfeven5  47908  dfodd7  47909  ixpv  49131  isoval2  49276  oppcciceq  49293  oppczeroo  49478  dfinito4  49742  lmdfval2  49896  cmdfval2  49897  initocmd  49910  termolmd  49911