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

Theorem abssdv 4002
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 1930 . 2 (𝜑 → ∀𝑥(𝜓𝑥𝐴))
3 abss 3994 . 2 ({𝑥𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓𝑥𝐴))
42, 3sylibr 233 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537  wcel 2106  {cab 2715  wss 3887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-v 3434  df-in 3894  df-ss 3904
This theorem is referenced by:  dfopifOLD  4801  opabssxpd  5634  fmpt  6984  eroprf  8604  cfslb2n  10024  rankcf  10533  genpv  10755  genpdm  10758  fimaxre3  11921  supadd  11943  supmul  11947  hashfacenOLD  14167  hashf1lem1OLD  14169  hashf1lem2  14170  mertenslem2  15597  4sqlem11  16656  lss1d  20225  lspsn  20264  lpval  22290  lpsscls  22292  ptuni2  22727  ptbasfi  22732  prdstopn  22779  xkopt  22806  tgpconncompeqg  23263  metrest  23680  mbfeqalem1  24805  limcfval  25036  nmosetre  29126  nmopsetretALT  30225  nmfnsetre  30239  sigaclcuni  32086  bnj849  32905  deranglem  33128  derangsn  33132  nosupno  33906  nosupbday  33908  noinfno  33921  noinfbday  33923  liness  34447  mblfinlem3  35816  ismblfin  35818  itg2addnclem  35828  areacirclem2  35866  sdclem2  35900  sdclem1  35901  ismtyval  35958  heibor1lem  35967  heibor1  35968  pmapglbx  37783  eldiophb  40579  hbtlem2  40949  upbdrech  42844
  Copyright terms: Public domain W3C validator