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

Theorem abssdv 4042
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 1919 . 2 (𝜑 → ∀𝑥(𝜓𝑥𝐴))
3 abss 4037 . 2 ({𝑥𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓𝑥𝐴))
42, 3sylibr 235 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  wcel 2105  {cab 2796  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949
This theorem is referenced by:  dfopif  4792  opabssxpd  5782  fmpt  6866  eroprf  8384  cfslb2n  9678  rankcf  10187  genpv  10409  genpdm  10412  fimaxre3  11575  supadd  11597  supmul  11601  hashfacen  13800  hashf1lem1  13801  hashf1lem2  13802  mertenslem2  15229  4sqlem11  16279  symgbas  18436  lss1d  19664  lspsn  19703  lpval  21675  lpsscls  21677  ptuni2  22112  ptbasfi  22117  prdstopn  22164  xkopt  22191  tgpconncompeqg  22647  metrest  23061  mbfeqalem1  24169  limcfval  24397  nmosetre  28468  nmopsetretALT  29567  nmfnsetre  29581  sigaclcuni  31276  bnj849  32096  deranglem  32310  derangsn  32314  nosupno  33100  nosupbday  33102  liness  33503  mblfinlem3  34812  ismblfin  34814  itg2addnclem  34824  areacirclem2  34864  sdclem2  34898  sdclem1  34899  ismtyval  34959  heibor1lem  34968  heibor1  34969  pmapglbx  36785  eldiophb  39232  hbtlem2  39602  upbdrech  41448
  Copyright terms: Public domain W3C validator