Theorem eqrdv 2232

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ wcel 2205

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 1496  ax-gen 1498  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqrdav  2233  abbi  2353  eqabdv  2365  csbcomg  3163  csbabg  3202  uneq1  3368  ineq1  3417  difin2  3485  difsn  3833  intmin4  3979  iunconstm  4001  iinconstm  4002  dfiun2g  4025  iindif2m  4061  iinin2m  4062  iunxsng  4069  iunxsngf  4071  iunpw  4603  opthprc  4803  inimasn  5182  dmsnopg  5236  dfco2a  5265  iotaeq  5323  fun11iun  5637  ssimaex  5740  unpreima  5804  respreima  5807  fconstfvm  5904  reldm  6382  suppimacnvfn  6448  suppcofn  6468  rntpos  6490  frecsuclem  6639  iserd  6795  erth  6815  ecidg  6835  mapdm0  6899  map0e  6922  ixpiinm  6961  pw2f1odclem  7089  fifo  7269  ordiso2  7328  ctssdccl  7404  ctssdc  7406  finacn  7513  pw1if  7537  exmidapne  7576  acnccim  7588  genpassl  7841  genpassu  7842  1idprl  7907  1idpru  7908  sup3exmid  9233  eqreznegel  9949  iccid  10261  fzsplit2  10387  fzsn  10403  fzpr  10415  uzsplit  10430  fzoval  10486  infssuzex  10597  frec2uzrand  10771  bitsmod  12646  bitscmp  12648  divsfval  13558  mhmpropd  13696  eqgid  13960  ghmmhmb  13988  ghmpropd  14017  ablnsg  14068  opprsubgg  14245  opprunitd  14272  unitpropdg  14310  opprsubrngg  14373  subsubrng2  14377  subrngpropd  14378  subsubrg2  14408  subrgpropd  14415  rhmpropd  14416  lssats2  14579  lsspropdg  14596  discld  15018  restsn  15062  restdis  15066  cndis  15123  cnpdis  15124  tx1cn  15151  tx2cn  15152  blpnf  15282  blininf  15306  blres  15316  xmetec  15319  metrest  15388  xmetxpbl  15390  cnbl0  15416  reopnap  15428  bl2ioo  15432  cncfmet  15474  limcdifap  15544  gausslemma2dlem1a  15948  ushgredgedg  16238  ushgredgedgloop  16240  clwwlknun  16453  eupth2lemsfi  16490