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

Theorem eqrdv 2083
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 1799 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2079 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 132 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1285   = wceq 1287  wcel 1436
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 1379  ax-gen 1381  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqrdav  2084  csbcomg  2943  csbabg  2978  uneq1  3136  ineq1  3183  difin2  3250  difsn  3556  intmin4  3698  iunconstm  3720  iinconstm  3721  dfiun2g  3744  iindif2m  3779  iinin2m  3780  iunxsng  3787  iunpw  4273  opthprc  4455  inimasn  4811  dmsnopg  4864  dfco2a  4893  iotaeq  4950  fun11iun  5230  ssimaex  5321  unpreima  5380  respreima  5383  fconstfvm  5469  reldm  5906  rntpos  5969  frecsuclem  6118  iserd  6263  erth  6281  ecidg  6301  mapdm0  6365  map0e  6388  ordiso2  6664  genpassl  7019  genpassu  7020  1idprl  7085  1idpru  7086  eqreznegel  9023  iccid  9267  fzsplit2  9388  fzsn  9403  fzpr  9413  uzsplit  9428  fzoval  9479  frec2uzrand  9732  infssuzex  10811
  Copyright terms: Public domain W3C validator