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 ⊢ (𝜑 → 𝐴 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqrdav  2237  abbi  2357  eqabdv  2369  csbcomg  3170  csbabg  3209  uneq1  3376  ineq1  3425  difin2  3493  difsn  3852  intmin4  3998  iunconstm  4020  iinconstm  4021  dfiun2g  4044  iindif2m  4080  iinin2m  4081  iunxsng  4088  iunxsngf  4090  iunpw  4626  opthprc  4826  inimasn  5205  dmsnopg  5259  dfco2a  5288  iotaeq  5346  fun11iun  5660  relndmfv  5728  ssimaex  5764  unpreima  5833  respreima  5836  fconstfvm  5933  reldm  6420  suppimacnvfn  6486  suppcofn  6506  rntpos  6528  frecsuclem  6677  iserd  6833  erth  6853  ecidg  6873  mapdm0  6937  mapfset  6945  map0e  6967  ixpiinm  7006  pw2f1odclem  7134  fifo  7314  ordiso2  7376  ctssdccl  7452  ctssdc  7454  finacn  7561  pw1if  7585  exmidapne  7627  acnccim  7639  genpassl  7892  genpassu  7893  1idprl  7958  1idpru  7959  sup3exmid  9290  indval0  9300  eqreznegel  10024  iccid  10338  fzsplit2  10466  fzsplit3  10469  fzsn  10483  fzpr  10495  uzsplit  10510  fzoval  10566  infssuzex  10677  frec2uzrand  10857  bitsmod  12742  bitscmp  12744  divsfval  13702  mhmpropd  13826  eqgid  14082  ghmmhmb  14110  ghmpropd  14139  cntzval  14147  resscntz  14160  ablnsg  14222  opprsubgg  14474  opprunitd  14501  unitpropdg  14539  opprsubrngg  14603  subsubrng2  14607  subrngpropd  14608  subsubrg2  14638  subrgpropd  14645  rhmpropd  14646  ringunitsap0  14678  drnguiap  14693  lssats2  14835  lsspropdg  14852  discld  15328  restsn  15372  restdis  15376  cndis  15433  cnpdis  15434  tx1cn  15461  tx2cn  15462  blpnf  15592  blininf  15616  blres  15626  xmetec  15629  metrest  15698  xmetxpbl  15700  cnbl0  15726  reopnap  15738  bl2ioo  15742  cncfmet  15784  limcdifap  15854  gausslemma2dlem1a  16343  ushgredgedg  16633  ushgredgedgloop  16635  clwwlknun  16848  eupth2lemsfi  16885