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

Theorem eqrdv 2080
 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 1796 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2076 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 132 1 (𝜑𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103  ∀wal 1283   = wceq 1285   ∈ wcel 1434 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-17 1460  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-cleq 2075 This theorem is referenced by:  eqrdav  2081  csbcomg  2930  csbabg  2964  uneq1  3120  ineq1  3167  difin2  3233  difsn  3531  intmin4  3672  iunconstm  3694  iinconstm  3695  dfiun2g  3718  iindif2m  3753  iinin2m  3754  iunxsng  3761  iunpw  4237  opthprc  4417  inimasn  4771  dmsnopg  4822  dfco2a  4851  iotaeq  4905  fun11iun  5178  ssimaex  5266  unpreima  5324  respreima  5327  fconstfvm  5411  reldm  5843  rntpos  5906  frecsuclem  6055  iserd  6198  erth  6216  ecidg  6236  ordiso2  6505  genpassl  6776  genpassu  6777  1idprl  6842  1idpru  6843  eqreznegel  8780  iccid  9024  fzsplit2  9145  fzsn  9160  fzpr  9170  uzsplit  9185  fzoval  9235  frec2uzrand  9487  infssuzex  10489
 Copyright terms: Public domain W3C validator