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

Theorem eqrdv 2168
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 1867 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2164 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 133 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1346   = wceq 1348  wcel 2141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163
This theorem is referenced by:  eqrdav  2169  csbcomg  3072  csbabg  3110  uneq1  3274  ineq1  3321  difin2  3389  difsn  3715  intmin4  3857  iunconstm  3879  iinconstm  3880  dfiun2g  3903  iindif2m  3938  iinin2m  3939  iunxsng  3946  iunxsngf  3948  iunpw  4463  opthprc  4660  inimasn  5026  dmsnopg  5080  dfco2a  5109  iotaeq  5166  fun11iun  5461  ssimaex  5555  unpreima  5618  respreima  5621  fconstfvm  5711  reldm  6162  rntpos  6233  frecsuclem  6382  iserd  6535  erth  6553  ecidg  6573  mapdm0  6637  map0e  6660  ixpiinm  6698  fifo  6953  ordiso2  7008  ctssdccl  7084  ctssdc  7086  genpassl  7473  genpassu  7474  1idprl  7539  1idpru  7540  sup3exmid  8860  eqreznegel  9560  iccid  9869  fzsplit2  9993  fzsn  10009  fzpr  10020  uzsplit  10035  fzoval  10091  frec2uzrand  10348  infssuzex  11891  mhmpropd  12676  discld  12889  restsn  12933  restdis  12937  cndis  12994  cnpdis  12995  tx1cn  13022  tx2cn  13023  blpnf  13153  blininf  13177  blres  13187  xmetec  13190  metrest  13259  xmetxpbl  13261  cnbl0  13287  reopnap  13291  bl2ioo  13295  cncfmet  13332  limcdifap  13384
  Copyright terms: Public domain W3C validator