ILE Home 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  6355  genpassl  6620  genpassu  6621  1idprl  6686  1idpru  6687  eqreznegel  8547  iccid  8792  fzsplit2  8912  fzsn  8927  fzpr  8937  uzsplit  8952  fzoval  9003  frec2uzrand  9165
  Copyright terms: Public domain W3C validator