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

Theorem abssi 4069
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 4066 . 2 {𝑥𝜑} ⊆ {𝑥𝑥𝐴}
3 abid2 2878 . 2 {𝑥𝑥𝐴} = 𝐴
42, 3sseqtri 4031 1 {𝑥𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  {cab 2713  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ss 3967
This theorem is referenced by:  ssab2  4078  intab  4977  opabss  5206  relopabiALT  5832  exse2  7940  opiota  8085  mpoexw  8104  fsplitfpar  8144  tfrlem8  8425  fiprc  9086  fival  9453  hartogslem1  9583  dmttrcl  9762  rnttrcl  9763  tz9.12lem1  9828  rankuni  9904  scott0  9927  r0weon  10053  alephval3  10151  aceq3lem  10161  dfac5lem4  10167  dfac5lem4OLD  10169  dfac2b  10172  cff  10289  cfsuc  10298  cff1  10299  cflim2  10304  cfss  10306  axdc3lem  10491  axdclem  10560  gruina  10859  nqpr  11055  infcvgaux1i  15894  4sqlem1  16987  sscpwex  17860  cssval  21701  topnex  23004  islocfin  23526  hauspwpwf1  23996  itg2lcl  25763  2sqlem7  27469  scutf  27858  isismt  28543  nmcexi  32046  opabssi  32626  lsmsnorb  33420  dispcmp  33859  cnre2csqima  33911  mppspstlem  35577  colinearex  36062  itg2addnclem  37679  itg2addnc  37682  eldiophb  42773
  Copyright terms: Public domain W3C validator