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  3443  rabtru  3646  nfccdeq  3738  csbgfi  3871  difeqri  4082  uneqri  4110  ineqri  4166  symdifass  4216  indifdi  4248  undif3  4254  csbcom  4374  csbab  4394  pwpr  4859  pwtp  4860  pwv  4862  uniun  4888  int0  4919  intun  4937  iuncom  4956  iuncom4  4957  iunin2  5028  iinun2  5030  iundif2  5031  iunun  5050  iunxun  5051  iunxiun  5054  iinpw  5063  inuni  5297  unipw  5405  xpiundi  5703  xpiundir  5704  iunxpf  5805  cnvuni  5843  dmiun  5870  dmuni  5871  idinxpres  6014  rniun  6113  xpdifid  6134  cnvresima  6196  imaco  6217  rnco  6218  rncoOLD  6219  imaindm  6265  dfmpt3  6634  imaiun  7201  unon  7783  opabex3d  7919  opabex3rd  7920  opabex3  7921  fparlem1  8064  fparlem2  8065  oarec  8499  ecid  8729  qsid  8730  mapval2  8822  ixpin  8873  onfin2  9153  unfilem1  9217  unifpw  9267  dfom5  9571  alephsuc2  10002  ackbij2  10164  isf33lem  10288  dffin7-2  10320  fin1a2lem6  10327  acncc  10362  fin41  10366  iunfo  10461  grutsk  10745  grothac  10753  grothtsk  10758  dfz2  12519  qexALT  12889  dfrp2  13322  om2uzrani  13887  hashkf  14267  divalglem4  16335  1nprm  16618  nsgacs  19103  oppgsubm  19303  oppgsubg  19304  oppgcntz  19305  pmtrprfvalrn  19429  opprsubg  20300  opprunit  20325  opprirred  20370  opprsubrng  20504  opprsubrg  20538  00lss  20904  dfprm2  21440  unocv  21647  iunocv  21648  00ply1bas  22192  toprntopon  22881  unisngl  23483  zcld  24770  iundisj  25517  plyun0  26170  aannenlem2  26305  dfz12s2  28496  eqid1  30554  choc0  31413  chocnul  31415  spanunsni  31666  lncnbd  32125  adjbd1o  32172  rnbra  32194  pjimai  32263  iunin1f  32643  iundisjf  32675  xrdifh  32870  iundisjfi  32886  opprnsg  33576  ccfldextdgrr  33849  cmpcref  34027  eulerpartgbij  34549  eulerpartlemr  34551  oddprm2  34832  dfdm5  35986  dfrn5  35987  dffix2  36116  fixcnv  36119  dfom5b  36123  fnimage  36140  brimg  36148  bj-csbsnlem  37145  bj-projun  37236  bj-pw0ALT  37291  bj-vjust  37297  finxp1o  37641  iundif1  37839  poimirlem26  37891  csbcom2fi  38373  dfsucmap3  38708  prtlem16  39239  sn-iotalem  42587  redvmptabs  42724  aaitgo  43513  imaiun1  44001  grumnueq  44637  nzss  44667  dfodd2  47990  dfeven5  48020  dfodd7  48021  ixpv  49243  isoval2  49388  oppcciceq  49405  oppczeroo  49590  dfinito4  49854  lmdfval2  50008  cmdfval2  50009  initocmd  50022  termolmd  50023