Theorem eqriv 2727

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 2723	. 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 2702

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

This theorem is referenced by:  eqid  2730  cbvabv  2800  cbvabw  2801  cbvab  2802  vjust  3451  rabtru  3659  nfccdeq  3752  csbgfi  3885  difeqri  4094  uneqri  4122  ineqri  4178  symdifass  4228  indifdi  4260  undif3  4266  csbcom  4386  csbab  4406  pwpr  4868  pwtp  4869  pwv  4871  uniun  4897  int0  4929  intun  4947  iuncom  4966  iuncom4  4967  iunin2  5038  iinun2  5040  iundif2  5041  iunun  5060  iunxun  5061  iunxiun  5064  iinpw  5073  inuni  5308  unipw  5413  xpiundi  5712  xpiundir  5713  iunxpf  5815  cnvuni  5853  dmiun  5880  dmuni  5881  idinxpres  6021  rniun  6123  xpdifid  6144  cnvresima  6206  imaco  6227  rnco  6228  imaindm  6275  dfmpt3  6655  imaiun  7222  unon  7809  opabex3d  7947  opabex3rd  7948  opabex3  7949  fparlem1  8094  fparlem2  8095  oarec  8529  ecid  8756  qsid  8757  mapval2  8848  ixpin  8899  onfin2  9186  unfilem1  9261  unifpw  9313  dfom5  9610  alephsuc2  10040  ackbij2  10202  isf33lem  10326  dffin7-2  10358  fin1a2lem6  10365  acncc  10400  fin41  10404  iunfo  10499  grutsk  10782  grothac  10790  grothtsk  10795  dfz2  12555  qexALT  12930  dfrp2  13362  om2uzrani  13924  hashkf  14304  divalglem4  16373  1nprm  16656  nsgacs  19101  oppgsubm  19301  oppgsubg  19302  oppgcntz  19303  pmtrprfvalrn  19425  opprsubg  20268  opprunit  20293  opprirred  20338  opprsubrng  20475  opprsubrg  20509  00lss  20854  dfprm2  21390  unocv  21596  iunocv  21597  00ply1bas  22131  toprntopon  22819  unisngl  23421  zcld  24709  iundisj  25456  plyun0  26109  aannenlem2  26244  eqid1  30403  choc0  31262  chocnul  31264  spanunsni  31515  lncnbd  31974  adjbd1o  32021  rnbra  32043  pjimai  32112  iunin1f  32493  iundisjf  32525  xrdifh  32710  iundisjfi  32726  opprnsg  33462  ccfldextdgrr  33674  cmpcref  33847  eulerpartgbij  34370  eulerpartlemr  34372  oddprm2  34653  dfdm5  35767  dfrn5  35768  dffix2  35900  fixcnv  35903  dfom5b  35907  fnimage  35924  brimg  35932  bj-csbsnlem  36898  bj-projun  36989  bj-pw0ALT  37044  bj-vjust  37050  finxp1o  37387  iundif1  37595  poimirlem26  37647  csbcom2fi  38129  prtlem16  38869  sn-iotalem  42216  redvmptabs  42355  aaitgo  43158  imaiun1  43647  grumnueq  44283  nzss  44313  dfodd2  47641  dfeven5  47671  dfodd7  47672  ixpv  48882  isoval2  49028  oppcciceq  49045  oppczeroo  49230  dfinito4  49494  lmdfval2  49648  cmdfval2  49649  initocmd  49662  termolmd  49663