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

Theorem abssi 3826
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 3823 . 2 {𝑥𝜑} ⊆ {𝑥𝑥𝐴}
3 abid2 2894 . 2 {𝑥𝑥𝐴} = 𝐴
42, 3sseqtri 3786 1 {𝑥𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  {cab 2757  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-in 3730  df-ss 3737
This theorem is referenced by:  ssab2  3835  intab  4641  opabss  4848  relopabiALT  5383  exse2  7252  opiota  7378  tfrlem8  7633  fiprc  8195  fival  8474  hartogslem1  8603  tz9.12lem1  8814  rankuni  8890  scott0  8913  r0weon  9035  alephval3  9133  aceq3lem  9143  dfac5lem4  9149  dfac2b  9153  dfac2OLD  9155  cff  9272  cfsuc  9281  cff1  9282  cflim2  9287  cfss  9289  axdc3lem  9474  axdclem  9543  gruina  9842  nqpr  10038  infcvgaux1i  14792  4sqlem1  15855  sscpwex  16678  symgval  18002  cssval  20239  topnex  21017  islocfin  21537  hauspwpwf1  22007  itg2lcl  23710  2sqlem7  25366  isismt  25646  nmcexi  29221  opabssi  29759  dispcmp  30262  cnre2csqima  30293  mppspstlem  31802  scutf  32252  colinearex  32500  cnfinltrel  33574  itg2addnclem  33789  itg2addnc  33792  eldiophb  37843
  Copyright terms: Public domain W3C validator