Theorem eqrdv 2202

Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)

Hypothesis

Ref	Expression
eqrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
eqrdv	⊢ (𝜑 → 𝐴 = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	alrimiv 1896	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2198	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1370   = wceq 1372   ∈ wcel 2175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197

This theorem is referenced by:  eqrdav  2203  eqabdv  2333  csbcomg  3115  csbabg  3154  uneq1  3319  ineq1  3366  difin2  3434  difsn  3769  intmin4  3912  iunconstm  3934  iinconstm  3935  dfiun2g  3958  iindif2m  3994  iinin2m  3995  iunxsng  4002  iunxsngf  4004  iunpw  4525  opthprc  4724  inimasn  5097  dmsnopg  5151  dfco2a  5180  iotaeq  5237  fun11iun  5537  ssimaex  5634  unpreima  5699  respreima  5702  fconstfvm  5792  reldm  6262  rntpos  6333  frecsuclem  6482  iserd  6636  erth  6656  ecidg  6676  mapdm0  6740  map0e  6763  ixpiinm  6801  pw2f1odclem  6913  fifo  7064  ordiso2  7119  ctssdccl  7195  ctssdc  7197  finacn  7298  exmidapne  7354  acnccim  7366  genpassl  7619  genpassu  7620  1idprl  7685  1idpru  7686  sup3exmid  9012  eqreznegel  9717  iccid  10029  fzsplit2  10154  fzsn  10170  fzpr  10181  uzsplit  10196  fzoval  10252  infssuzex  10357  frec2uzrand  10531  bitsmod  12186  bitscmp  12188  divsfval  13078  mhmpropd  13216  eqgid  13480  ghmmhmb  13508  ghmpropd  13537  ablnsg  13588  opprsubgg  13764  opprunitd  13790  unitpropdg  13828  opprsubrngg  13891  subsubrng2  13895  subrngpropd  13896  subsubrg2  13926  subrgpropd  13933  rhmpropd  13934  lssats2  14094  lsspropdg  14111  discld  14526  restsn  14570  restdis  14574  cndis  14631  cnpdis  14632  tx1cn  14659  tx2cn  14660  blpnf  14790  blininf  14814  blres  14824  xmetec  14827  metrest  14896  xmetxpbl  14898  cnbl0  14924  reopnap  14936  bl2ioo  14940  cncfmet  14982  limcdifap  15052  gausslemma2dlem1a  15453