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

Theorem abssdv 4026
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) (Proof shortened by SN, 22-Dec-2024.)
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 (𝜑 → (𝜓𝑥𝐴))
21ss2abdv 4021 . 2 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝑥𝐴})
3 abid1 2871 . 2 𝐴 = {𝑥𝑥𝐴}
42, 3sseqtrrdi 3996 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  {cab 2710  wss 3911
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928
This theorem is referenced by:  dfopif  4828  opabssxpd  5680  fmpt  7059  eroprf  8757  cfslb2n  10209  rankcf  10718  genpv  10940  genpdm  10943  fimaxre3  12106  supadd  12128  supmul  12132  hashfacenOLD  14358  hashf1lem1OLD  14360  hashf1lem2  14361  mertenslem2  15775  4sqlem11  16832  lss1d  20439  lspsn  20478  lpval  22506  lpsscls  22508  ptuni2  22943  ptbasfi  22948  prdstopn  22995  xkopt  23022  tgpconncompeqg  23479  metrest  23896  mbfeqalem1  25021  limcfval  25252  nosupno  27067  nosupbday  27069  noinfno  27082  noinfbday  27084  addsproplem2  27304  addsunif  27332  negsid  27361  mulsproplem10  27410  nmosetre  29748  nmopsetretALT  30847  nmfnsetre  30861  sigaclcuni  32774  bnj849  33594  deranglem  33817  derangsn  33821  liness  34776  mblfinlem3  36163  ismblfin  36165  itg2addnclem  36175  areacirclem2  36213  sdclem2  36247  sdclem1  36248  ismtyval  36305  heibor1lem  36314  heibor1  36315  pmapglbx  38278  eldiophb  41123  hbtlem2  41494  oaun3lem1  41733  oaun3lem2  41734  upbdrech  43626
  Copyright terms: Public domain W3C validator