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

Theorem abssi 3874
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 3871 . 2 {𝑥𝜑} ⊆ {𝑥𝑥𝐴}
3 abid2 2929 . 2 {𝑥𝑥𝐴} = 𝐴
42, 3sseqtri 3834 1 {𝑥𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  {cab 2792  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-in 3776  df-ss 3783
This theorem is referenced by:  ssab2  3883  intab  4699  opabss  4908  relopabiALT  5448  exse2  7335  opiota  7461  tfrlem8  7716  fiprc  8278  fival  8557  hartogslem1  8686  tz9.12lem1  8897  rankuni  8973  scott0  8996  r0weon  9118  alephval3  9216  aceq3lem  9226  dfac5lem4  9232  dfac2b  9236  dfac2OLD  9238  cff  9355  cfsuc  9364  cff1  9365  cflim2  9370  cfss  9372  axdc3lem  9557  axdclem  9626  gruina  9925  nqpr  10121  infcvgaux1i  14811  4sqlem1  15869  sscpwex  16679  symgval  18000  cssval  20236  topnex  21014  islocfin  21534  hauspwpwf1  22004  itg2lcl  23708  2sqlem7  25363  isismt  25643  nmcexi  29213  opabssi  29750  dispcmp  30251  cnre2csqima  30282  mppspstlem  31791  scutf  32240  colinearex  32488  cnfinltrel  33557  itg2addnclem  33773  itg2addnc  33776  eldiophb  37822
  Copyright terms: Public domain W3C validator