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

Theorem abssi 4000
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 3997 . 2 {𝑥𝜑} ⊆ {𝑥𝑥𝐴}
3 abid2 2935 . 2 {𝑥𝑥𝐴} = 𝐴
42, 3sseqtri 3954 1 {𝑥𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  {cab 2779  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  ssab2  4009  intab  4871  opabss  5097  relopabiALT  5663  exse2  7608  opiota  7743  mpoexw  7763  fsplitfpar  7801  tfrlem8  8007  fiprc  8582  fival  8864  hartogslem1  8994  tz9.12lem1  9204  rankuni  9280  scott0  9303  r0weon  9427  alephval3  9525  aceq3lem  9535  dfac5lem4  9541  dfac2b  9545  cff  9663  cfsuc  9672  cff1  9673  cflim2  9678  cfss  9680  axdc3lem  9865  axdclem  9934  gruina  10233  nqpr  10429  infcvgaux1i  15208  4sqlem1  16278  sscpwex  17081  cssval  20375  topnex  21605  islocfin  22126  hauspwpwf1  22596  itg2lcl  24335  2sqlem7  26012  isismt  26332  nmcexi  29813  opabssi  30381  lsmsnorb  31003  dispcmp  31216  cnre2csqima  31268  mppspstlem  32932  scutf  33387  colinearex  33635  itg2addnclem  35107  itg2addnc  35110  eldiophb  39691
  Copyright terms: Public domain W3C validator