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 1799	1 ⊢ 𝐴 = 𝐵

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqid  2737  cbvabv  2812  cbvabw  2813  cbvab  2814  vjust  3481  rabtru  3689  nfccdeq  3784  csbgfi  3919  difeqri  4128  uneqri  4156  ineqri  4212  symdifass  4262  indifdi  4294  undif3  4300  csbcom  4420  csbab  4440  pwpr  4901  pwtp  4902  pwv  4904  uniun  4930  int0  4962  intun  4980  iuncom  4999  iuncom4  5000  iunin2  5071  iinun2  5073  iundif2  5074  iunun  5093  iunxun  5094  iunxiun  5097  iinpw  5106  inuni  5350  unipw  5455  xpiundi  5756  xpiundir  5757  iunxpf  5859  cnvuni  5897  dmiun  5924  dmuni  5925  idinxpres  6065  rniun  6167  xpdifid  6188  cnvresima  6250  imaco  6271  rnco  6272  imaindm  6319  dfmpt3  6702  imaiun  7265  unon  7851  opabex3d  7990  opabex3rd  7991  opabex3  7992  fparlem1  8137  fparlem2  8138  oarec  8600  ecid  8822  qsid  8823  mapval2  8912  ixpin  8963  onfin2  9268  unfilem1  9343  unifpw  9395  dfom5  9690  alephsuc2  10120  ackbij2  10282  isf33lem  10406  dffin7-2  10438  fin1a2lem6  10445  acncc  10480  fin41  10484  iunfo  10579  grutsk  10862  grothac  10870  grothtsk  10875  dfz2  12632  qexALT  13006  dfrp2  13436  om2uzrani  13993  hashkf  14371  divalglem4  16433  1nprm  16716  nsgacs  19180  oppgsubm  19381  oppgsubg  19382  oppgcntz  19383  pmtrprfvalrn  19506  opprsubg  20352  opprunit  20377  opprirred  20422  opprsubrng  20559  opprsubrg  20593  00lss  20939  dfprm2  21484  unocv  21698  iunocv  21699  00ply1bas  22241  toprntopon  22931  unisngl  23535  zcld  24835  iundisj  25583  plyun0  26236  aannenlem2  26371  eqid1  30486  choc0  31345  chocnul  31347  spanunsni  31598  lncnbd  32057  adjbd1o  32104  rnbra  32126  pjimai  32195  iunin1f  32570  iundisjf  32602  xrdifh  32782  iundisjfi  32798  opprnsg  33512  ccfldextdgrr  33722  cmpcref  33849  eulerpartgbij  34374  eulerpartlemr  34376  oddprm2  34670  dfdm5  35773  dfrn5  35774  dffix2  35906  fixcnv  35909  dfom5b  35913  fnimage  35930  brimg  35938  bj-csbsnlem  36904  bj-projun  36995  bj-pw0ALT  37050  bj-vjust  37056  finxp1o  37393  iundif1  37601  poimirlem26  37653  csbcom2fi  38135  prtlem16  38870  sn-iotalem  42260  redvmptabs  42390  aaitgo  43174  imaiun1  43664  grumnueq  44306  nzss  44336  dfodd2  47623  dfeven5  47653  dfodd7  47654