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  7375  ctssdccl  7451  ctssdc  7453  finacn  7560  pw1if  7584  exmidapne  7626  acnccim  7638  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  sup3exmid  9287  indval0  9297  eqreznegel  10014  iccid  10327  fzsplit2  10455  fzsplit3  10458  fzsn  10472  fzpr  10484  uzsplit  10499  fzoval  10555  infssuzex  10666  frec2uzrand  10842  bitsmod  12723  bitscmp  12725  divsfval  13649  mhmpropd  13773  eqgid  14029  ghmmhmb  14057  ghmpropd  14086  ablnsg  14138  opprsubgg  14390  opprunitd  14417  unitpropdg  14455  opprsubrngg  14519  subsubrng2  14523  subrngpropd  14524  subsubrg2  14554  subrgpropd  14561  rhmpropd  14562  ringunitsap0  14594  drnguiap  14609  lssats2  14751  lsspropdg  14768  discld  15237  restsn  15281  restdis  15285  cndis  15342  cnpdis  15343  tx1cn  15370  tx2cn  15371  blpnf  15501  blininf  15525  blres  15535  xmetec  15538  metrest  15607  xmetxpbl  15609  cnbl0  15635  reopnap  15647  bl2ioo  15651  cncfmet  15693  limcdifap  15763  gausslemma2dlem1a  16177  ushgredgedg  16467  ushgredgedgloop  16469  clwwlknun  16682  eupth2lemsfi  16719