Theorem eqrdv 2194

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 1888	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2190	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1362   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqrdav  2195  eqabdv  2325  csbcomg  3107  csbabg  3146  uneq1  3311  ineq1  3358  difin2  3426  difsn  3760  intmin4  3903  iunconstm  3925  iinconstm  3926  dfiun2g  3949  iindif2m  3985  iinin2m  3986  iunxsng  3993  iunxsngf  3995  iunpw  4516  opthprc  4715  inimasn  5088  dmsnopg  5142  dfco2a  5171  iotaeq  5228  fun11iun  5528  ssimaex  5625  unpreima  5690  respreima  5693  fconstfvm  5783  reldm  6253  rntpos  6324  frecsuclem  6473  iserd  6627  erth  6647  ecidg  6667  mapdm0  6731  map0e  6754  ixpiinm  6792  pw2f1odclem  6904  fifo  7055  ordiso2  7110  ctssdccl  7186  ctssdc  7188  finacn  7289  exmidapne  7345  acnccim  7357  genpassl  7610  genpassu  7611  1idprl  7676  1idpru  7677  sup3exmid  9003  eqreznegel  9707  iccid  10019  fzsplit2  10144  fzsn  10160  fzpr  10171  uzsplit  10186  fzoval  10242  infssuzex  10342  frec2uzrand  10516  bitsmod  12140  bitscmp  12142  divsfval  13032  mhmpropd  13170  eqgid  13434  ghmmhmb  13462  ghmpropd  13491  ablnsg  13542  opprsubgg  13718  opprunitd  13744  unitpropdg  13782  opprsubrngg  13845  subsubrng2  13849  subrngpropd  13850  subsubrg2  13880  subrgpropd  13887  rhmpropd  13888  lssats2  14048  lsspropdg  14065  discld  14480  restsn  14524  restdis  14528  cndis  14585  cnpdis  14586  tx1cn  14613  tx2cn  14614  blpnf  14744  blininf  14768  blres  14778  xmetec  14781  metrest  14850  xmetxpbl  14852  cnbl0  14878  reopnap  14890  bl2ioo  14894  cncfmet  14936  limcdifap  15006  gausslemma2dlem1a  15407