Theorem eqrdv 2236

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqrdav  2237  abbi  2357  eqabdv  2369  csbcomg  3170  csbabg  3209  uneq1  3376  ineq1  3425  difin2  3493  difsn  3850  intmin4  3996  iunconstm  4018  iinconstm  4019  dfiun2g  4042  iindif2m  4078  iinin2m  4079  iunxsng  4086  iunxsngf  4088  iunpw  4624  opthprc  4824  inimasn  5203  dmsnopg  5257  dfco2a  5286  iotaeq  5344  fun11iun  5658  ssimaex  5761  unpreima  5827  respreima  5830  fconstfvm  5927  reldm  6413  suppimacnvfn  6479  suppcofn  6499  rntpos  6521  frecsuclem  6670  iserd  6826  erth  6846  ecidg  6866  mapdm0  6930  mapfset  6938  map0e  6960  ixpiinm  6999  pw2f1odclem  7127  fifo  7307  ordiso2  7368  ctssdccl  7444  ctssdc  7446  finacn  7553  pw1if  7577  exmidapne  7619  acnccim  7631  genpassl  7884  genpassu  7885  1idprl  7950  1idpru  7951  sup3exmid  9280  eqreznegel  9996  iccid  10309  fzsplit2  10436  fzsplit3  10439  fzsn  10453  fzpr  10465  uzsplit  10480  fzoval  10536  infssuzex  10647  frec2uzrand  10823  bitsmod  12704  bitscmp  12706  divsfval  13629  mhmpropd  13753  eqgid  14009  ghmmhmb  14037  ghmpropd  14066  ablnsg  14118  opprsubgg  14366  opprunitd  14393  unitpropdg  14431  opprsubrngg  14495  subsubrng2  14499  subrngpropd  14500  subsubrg2  14530  subrgpropd  14537  rhmpropd  14538  ringunitsap0  14570  drnguiap  14585  lssats2  14726  lsspropdg  14743  discld  15163  restsn  15207  restdis  15211  cndis  15268  cnpdis  15269  tx1cn  15296  tx2cn  15297  blpnf  15427  blininf  15451  blres  15461  xmetec  15464  metrest  15533  xmetxpbl  15535  cnbl0  15561  reopnap  15573  bl2ioo  15577  cncfmet  15619  limcdifap  15689  gausslemma2dlem1a  16094  ushgredgedg  16384  ushgredgedgloop  16386  clwwlknun  16599  eupth2lemsfi  16636