MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abssi Structured version   Visualization version   GIF version

Theorem abssi 3639
Description: Inference of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
Hypothesis
Ref Expression
abssi.1 (𝜑𝑥𝐴)
Assertion
Ref Expression
abssi {𝑥𝜑} ⊆ 𝐴
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem abssi
StepHypRef Expression
1 abssi.1 . . 3 (𝜑𝑥𝐴)
21ss2abi 3636 . 2 {𝑥𝜑} ⊆ {𝑥𝑥𝐴}
3 abid2 2731 . 2 {𝑥𝑥𝐴} = 𝐴
42, 3sseqtri 3599 1 {𝑥𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  {cab 2595  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553
This theorem is referenced by:  ssab2  3648  intab  4436  opabss  4640  relopabi  5155  exse2  6975  opiota  7095  tfrlem8  7344  fiprc  7901  fival  8178  hartogslem1  8307  tz9.12lem1  8510  rankuni  8586  scott0  8609  r0weon  8695  alephval3  8793  aceq3lem  8803  dfac5lem4  8809  dfac2  8813  cff  8930  cfsuc  8939  cff1  8940  cflim2  8945  cfss  8947  axdc3lem  9132  axdclem  9201  gruina  9496  nqpr  9692  infcvgaux1i  14376  4sqlem1  15438  sscpwex  16246  symgval  17570  cssval  19792  islocfin  21077  hauspwpwf1  21548  itg2lcl  23244  2sqlem7  24893  isismt  25174  nmcexi  28062  dispcmp  29047  cnre2csqima  29078  mppspstlem  30515  colinearex  31130  bj-topnex  32030  itg2addnclem  32414  itg2addnc  32417  eldiophb  36121
  Copyright terms: Public domain W3C validator