Theorem eqrdv 2227

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqrdav  2228  eqabdv  2358  csbcomg  3148  csbabg  3187  uneq1  3352  ineq1  3399  difin2  3467  difsn  3808  intmin4  3954  iunconstm  3976  iinconstm  3977  dfiun2g  4000  iindif2m  4036  iinin2m  4037  iunxsng  4044  iunxsngf  4046  iunpw  4575  opthprc  4775  inimasn  5152  dmsnopg  5206  dfco2a  5235  iotaeq  5293  fun11iun  5601  ssimaex  5703  unpreima  5768  respreima  5771  fconstfvm  5867  reldm  6344  rntpos  6418  frecsuclem  6567  iserd  6723  erth  6743  ecidg  6763  mapdm0  6827  map0e  6850  ixpiinm  6888  pw2f1odclem  7015  fifo  7170  ordiso2  7225  ctssdccl  7301  ctssdc  7303  finacn  7409  pw1if  7433  exmidapne  7469  acnccim  7481  genpassl  7734  genpassu  7735  1idprl  7800  1idpru  7801  sup3exmid  9127  eqreznegel  9838  iccid  10150  fzsplit2  10275  fzsn  10291  fzpr  10302  uzsplit  10317  fzoval  10373  infssuzex  10483  frec2uzrand  10657  bitsmod  12507  bitscmp  12509  divsfval  13401  mhmpropd  13539  eqgid  13803  ghmmhmb  13831  ghmpropd  13860  ablnsg  13911  opprsubgg  14087  opprunitd  14114  unitpropdg  14152  opprsubrngg  14215  subsubrng2  14219  subrngpropd  14220  subsubrg2  14250  subrgpropd  14257  rhmpropd  14258  lssats2  14418  lsspropdg  14435  discld  14850  restsn  14894  restdis  14898  cndis  14955  cnpdis  14956  tx1cn  14983  tx2cn  14984  blpnf  15114  blininf  15138  blres  15148  xmetec  15151  metrest  15220  xmetxpbl  15222  cnbl0  15248  reopnap  15260  bl2ioo  15264  cncfmet  15306  limcdifap  15376  gausslemma2dlem1a  15777  ushgredgedg  16065  ushgredgedgloop  16067  clwwlknun  16236