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  5285  unipw  5395  xpiundi  5693  xpiundir  5694  iunxpf  5795  cnvuni  5833  dmiun  5860  dmuni  5861  idinxpres  6004  rniun  6103  xpdifid  6124  cnvresima  6186  imaco  6207  rnco  6208  rncoOLD  6209  imaindm  6255  dfmpt3  6624  imaiun  7191  unon  7773  opabex3d  7909  opabex3rd  7910  opabex3  7911  fparlem1  8053  fparlem2  8054  oarec  8488  ecid  8718  qsid  8719  mapval2  8811  ixpin  8862  onfin2  9142  unfilem1  9206  unifpw  9256  dfom5  9560  alephsuc2  9991  ackbij2  10153  isf33lem  10277  dffin7-2  10309  fin1a2lem6  10316  acncc  10351  fin41  10355  iunfo  10450  grutsk  10734  grothac  10742  grothtsk  10747  dfz2  12508  qexALT  12878  dfrp2  13311  om2uzrani  13876  hashkf  14256  divalglem4  16324  1nprm  16607  nsgacs  19095  oppgsubm  19295  oppgsubg  19296  oppgcntz  19297  pmtrprfvalrn  19421  opprsubg  20290  opprunit  20315  opprirred  20360  opprsubrng  20494  opprsubrg  20528  00lss  20894  dfprm2  21430  unocv  21637  iunocv  21638  00ply1bas  22181  toprntopon  22868  unisngl  23470  zcld  24757  iundisj  25493  plyun0  26143  aannenlem2  26277  dfz12s2  28468  eqid1  30526  choc0  31386  chocnul  31388  spanunsni  31639  lncnbd  32098  adjbd1o  32145  rnbra  32167  pjimai  32236  iunin1f  32616  iundisjf  32648  xrdifh  32843  iundisjfi  32859  opprnsg  33549  ccfldextdgrr  33822  cmpcref  34000  eulerpartgbij  34522  eulerpartlemr  34524  oddprm2  34805  dfdm5  35961  dfrn5  35962  dffix2  36091  fixcnv  36094  dfom5b  36098  fnimage  36115  brimg  36123  bj-csbsnlem  37208  bj-projun  37299  bj-pw0ALT  37354  bj-vjust  37360  finxp1o  37704  iundif1  37906  poimirlem26  37958  csbcom2fi  38440  dfsucmap3  38775  prtlem16  39306  sn-iotalem  42654  redvmptabs  42791  aaitgo  43593  imaiun1  44081  grumnueq  44717  nzss  44747  dfodd2  48070  dfeven5  48100  dfodd7  48101  ixpv  49323  isoval2  49468  oppcciceq  49485  oppczeroo  49670  dfinito4  49934  lmdfval2  50088  cmdfval2  50089  initocmd  50102  termolmd  50103