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

Theorem abssdv 3884
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)
Hypothesis
Ref Expression
abssdv.1 (𝜑 → (𝜓𝑥𝐴))
Assertion
Ref Expression
abssdv (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Distinct variable groups:   𝜑,𝑥   𝑥,𝐴
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abssdv
StepHypRef Expression
1 abssdv.1 . . 3 (𝜑 → (𝜓𝑥𝐴))
21alrimiv 2018 . 2 (𝜑 → ∀𝑥(𝜓𝑥𝐴))
3 abss 3879 . 2 ({𝑥𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓𝑥𝐴))
42, 3sylibr 225 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635  wcel 2157  {cab 2803  wss 3780
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 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
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 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-in 3787  df-ss 3794
This theorem is referenced by:  dfopif  4603  opabssxpd  5553  fmpt  6612  eroprf  8091  cfslb2n  9385  rankcf  9894  genpv  10116  genpdm  10119  fimaxre3  11265  supadd  11286  supmul  11290  hashfacen  13475  hashf1lem1  13476  hashf1lem2  13477  mertenslem2  14858  4sqlem11  15896  symgbas  18021  lss1d  19190  lspsn  19229  lpval  21178  lpsscls  21180  ptuni2  21614  ptbasfi  21619  prdstopn  21666  xkopt  21693  tgpconncompeqg  22149  metrest  22563  mbfeqalem1  23645  limcfval  23873  nmosetre  27970  nmopsetretALT  29073  nmfnsetre  29087  sigaclcuni  30529  bnj849  31340  deranglem  31493  derangsn  31497  nosupno  32192  nosupbday  32194  liness  32595  mblfinlem3  33780  ismblfin  33782  itg2addnclem  33792  areacirclem2  33832  sdclem2  33868  sdclem1  33869  ismtyval  33929  heibor1lem  33938  heibor1  33939  pmapglbx  35568  eldiophb  37840  hbtlem2  38213  upbdrech  40018
  Copyright terms: Public domain W3C validator