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

Theorem abssdv 4048
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 1921 . 2 (𝜑 → ∀𝑥(𝜓𝑥𝐴))
3 abss 4043 . 2 ({𝑥𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓𝑥𝐴))
42, 3sylibr 235 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528  wcel 2106  {cab 2802  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-in 3946  df-ss 3955
This theorem is referenced by:  dfopif  4798  opabssxpd  5787  fmpt  6869  eroprf  8388  cfslb2n  9682  rankcf  10191  genpv  10413  genpdm  10416  fimaxre3  11579  supadd  11601  supmul  11605  hashfacen  13805  hashf1lem1  13806  hashf1lem2  13807  mertenslem2  15233  4sqlem11  16283  symgbas  18430  lss1d  19657  lspsn  19696  lpval  21663  lpsscls  21665  ptuni2  22100  ptbasfi  22105  prdstopn  22152  xkopt  22179  tgpconncompeqg  22635  metrest  23049  mbfeqalem1  24157  limcfval  24385  nmosetre  28456  nmopsetretALT  29555  nmfnsetre  29569  sigaclcuni  31264  bnj849  32084  deranglem  32298  derangsn  32302  nosupno  33088  nosupbday  33090  liness  33491  mblfinlem3  34799  ismblfin  34801  itg2addnclem  34811  areacirclem2  34851  sdclem2  34886  sdclem1  34887  ismtyval  34947  heibor1lem  34956  heibor1  34957  pmapglbx  36773  eldiophb  39216  hbtlem2  39586  upbdrech  41434
  Copyright terms: Public domain W3C validator