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

Theorem eqrdv 2038
 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 1754 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2034 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 137 1 (𝜑𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  eqrdav  2039  csbcomg  2873  csbabg  2907  uneq1  3090  ineq1  3131  difin2  3199  difsn  3501  intmin4  3643  iunconstm  3665  iinconstm  3666  dfiun2g  3689  iindif2m  3724  iinin2m  3725  iunxsng  3732  iunpw  4211  opthprc  4391  inimasn  4741  dmsnopg  4792  dfco2a  4821  iotaeq  4875  fun11iun  5147  ssimaex  5234  unpreima  5292  respreima  5295  fconstfvm  5379  reldm  5812  rntpos  5872  frecsuclem3  5990  iserd  6132  erth  6150  ecidg  6170  ordiso2  6357  genpassl  6622  genpassu  6623  1idprl  6688  1idpru  6689  eqreznegel  8549  iccid  8794  fzsplit2  8914  fzsn  8929  fzpr  8939  uzsplit  8954  fzoval  9005  frec2uzrand  9191
 Copyright terms: Public domain W3C validator