ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqrdv GIF version

Theorem eqrdv 2098
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
StepHypRef Expression
1 eqrdv.1 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
21alrimiv 1813 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2094 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 133 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1297   = wceq 1299  wcel 1448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-17 1474  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-cleq 2093
This theorem is referenced by:  eqrdav  2099  csbcomg  2976  csbabg  3011  uneq1  3170  ineq1  3217  difin2  3285  difsn  3604  intmin4  3746  iunconstm  3768  iinconstm  3769  dfiun2g  3792  iindif2m  3827  iinin2m  3828  iunxsng  3835  iunxsngf  3837  iunpw  4339  opthprc  4528  inimasn  4892  dmsnopg  4946  dfco2a  4975  iotaeq  5032  fun11iun  5322  ssimaex  5414  unpreima  5477  respreima  5480  fconstfvm  5570  reldm  6014  rntpos  6084  frecsuclem  6233  iserd  6385  erth  6403  ecidg  6423  mapdm0  6487  map0e  6510  ixpiinm  6548  ordiso2  6835  ctssdclemr  6911  ctssdc  6912  genpassl  7233  genpassu  7234  1idprl  7299  1idpru  7300  sup3exmid  8573  eqreznegel  9256  iccid  9549  fzsplit2  9671  fzsn  9687  fzpr  9698  uzsplit  9713  fzoval  9766  frec2uzrand  10019  infssuzex  11437  discld  12087  restsn  12131  restdis  12135  cndis  12191  cnpdis  12192  tx1cn  12219  tx2cn  12220  blpnf  12328  blininf  12352  blres  12362  xmetec  12365  metrest  12434  cnbl0  12456  bl2ioo  12461  cncfmet  12492  limcdifap  12512
  Copyright terms: Public domain W3C validator