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

Theorem abssdv 3709
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 1895 . 2 (𝜑 → ∀𝑥(𝜓𝑥𝐴))
3 abss 3704 . 2 ({𝑥𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓𝑥𝐴))
42, 3sylibr 224 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  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:  dfopif  4430  opabssxpd  5370  fmpt  6421  eroprf  7888  cfslb2n  9128  rankcf  9637  genpv  9859  genpdm  9862  fimaxre3  11008  supadd  11029  supmul  11033  hashfacen  13276  hashf1lem1  13277  hashf1lem2  13278  mertenslem2  14661  4sqlem11  15706  symgbas  17846  lss1d  19011  lspsn  19050  lpval  20991  lpsscls  20993  ptuni2  21427  ptbasfi  21432  prdstopn  21479  xkopt  21506  tgpconncompeqg  21962  metrest  22376  mbfeqalem  23454  limcfval  23681  nmosetre  27747  nmopsetretALT  28850  nmfnsetre  28864  sigaclcuni  30309  bnj849  31121  deranglem  31274  derangsn  31278  nosupno  31974  nosupbday  31976  liness  32377  mblfinlem3  33578  ismblfin  33580  itg2addnclem  33591  areacirclem2  33631  sdclem2  33668  sdclem1  33669  ismtyval  33729  heibor1lem  33738  heibor1  33739  pmapglbx  35373  eldiophb  37637  hbtlem2  38011  upbdrech  39833
  Copyright terms: Public domain W3C validator