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  3147  csbabg  3186  uneq1  3351  ineq1  3398  difin2  3466  difsn  3805  intmin4  3951  iunconstm  3973  iinconstm  3974  dfiun2g  3997  iindif2m  4033  iinin2m  4034  iunxsng  4041  iunxsngf  4043  iunpw  4571  opthprc  4770  inimasn  5146  dmsnopg  5200  dfco2a  5229  iotaeq  5287  fun11iun  5595  ssimaex  5697  unpreima  5762  respreima  5765  fconstfvm  5861  reldm  6338  rntpos  6409  frecsuclem  6558  iserd  6714  erth  6734  ecidg  6754  mapdm0  6818  map0e  6841  ixpiinm  6879  pw2f1odclem  7003  fifo  7158  ordiso2  7213  ctssdccl  7289  ctssdc  7291  finacn  7397  pw1if  7421  exmidapne  7457  acnccim  7469  genpassl  7722  genpassu  7723  1idprl  7788  1idpru  7789  sup3exmid  9115  eqreznegel  9821  iccid  10133  fzsplit2  10258  fzsn  10274  fzpr  10285  uzsplit  10300  fzoval  10356  infssuzex  10465  frec2uzrand  10639  bitsmod  12482  bitscmp  12484  divsfval  13376  mhmpropd  13514  eqgid  13778  ghmmhmb  13806  ghmpropd  13835  ablnsg  13886  opprsubgg  14062  opprunitd  14089  unitpropdg  14127  opprsubrngg  14190  subsubrng2  14194  subrngpropd  14195  subsubrg2  14225  subrgpropd  14232  rhmpropd  14233  lssats2  14393  lsspropdg  14410  discld  14825  restsn  14869  restdis  14873  cndis  14930  cnpdis  14931  tx1cn  14958  tx2cn  14959  blpnf  15089  blininf  15113  blres  15123  xmetec  15126  metrest  15195  xmetxpbl  15197  cnbl0  15223  reopnap  15235  bl2ioo  15239  cncfmet  15281  limcdifap  15351  gausslemma2dlem1a  15752  ushgredgedg  16039  ushgredgedgloop  16041