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

Theorem abssi 3710
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 3707 . 2 {𝑥𝜑} ⊆ {𝑥𝑥𝐴}
3 abid2 2774 . 2 {𝑥𝑥𝐴} = 𝐴
42, 3sseqtri 3670 1 {𝑥𝜑} ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  {cab 2637  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621
This theorem is referenced by:  ssab2  3719  intab  4539  opabss  4747  relopabiALT  5279  exse2  7147  opiota  7273  tfrlem8  7525  fiprc  8080  fival  8359  hartogslem1  8488  tz9.12lem1  8688  rankuni  8764  scott0  8787  r0weon  8873  alephval3  8971  aceq3lem  8981  dfac5lem4  8987  dfac2  8991  cff  9108  cfsuc  9117  cff1  9118  cflim2  9123  cfss  9125  axdc3lem  9310  axdclem  9379  gruina  9678  nqpr  9874  infcvgaux1i  14633  4sqlem1  15699  sscpwex  16522  symgval  17845  cssval  20074  topnex  20848  islocfin  21368  hauspwpwf1  21838  itg2lcl  23539  2sqlem7  25194  isismt  25474  nmcexi  29013  opabssi  29551  dispcmp  30054  cnre2csqima  30085  mppspstlem  31594  scutf  32044  colinearex  32292  itg2addnclem  33591  itg2addnc  33594  eldiophb  37637
  Copyright terms: Public domain W3C validator