Theorem abssdv 4015

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

Step	Hyp	Ref	Expression
1		abssdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴))
2	1	ss2abdv 4013	. 2 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴})
3		abid1 2896	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
4	2, 3	sseqtrrdi 3972	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {cab 2738   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916

This theorem is used by:  dfopif  4830  abexd  5290  opabssxpd  5702  fmpt  7104  fabexd  7935  eroprf  8816  cfslb2n  10271  axdc2lem  10451  rankcf  10787  genpv  11009  genpdm  11012  fimaxre3  12186  supadd  12208  supmul  12212  hashf1lem2  14522  mertenslem2  15975  4sqlem11  17048  lss1d  21148  lspsn  21187  lpval  23365  lpsscls  23367  ptuni2  23803  ptbasfi  23808  prdstopn  23855  xkopt  23882  tgpconncompeqg  24339  metrest  24751  mbfeqalem1  25870  limcfval  26100  nosupno  27940  nosupbday  27942  noinfno  27955  noinfbday  27957  addsproplem2  28236  addsuniflem  28267  addbdaylem  28283  negsid  28307  mulsproplem9  28390  sltmuls1  28413  sltmuls2  28414  precsexlem8  28480  precsexlem11  28483  onaddscl  28543  onmulscl  28544  recut  28760  elreno2  28761  nmosetre  31246  nmopsetretALT  32345  nmfnsetre  32359  sigaclcuni  34629  bnj849  35435  vonf1oonfo  35713  deranglem  35746  derangsn  35750  liness  36726  nmulprop  36771  mblfinlem3  38409  ismblfin  38411  itg2addnclem  38421  areacirclem2  38459  sdclem2  38493  sdclem1  38494  ismtyval  38551  heibor1lem  38560  heibor1  38561  pmapglbx  40643  eldiophb  43603  hbtlem2  43966  oaun3lem1  44216  oaun3lem2  44217  upbdrech  46139  hoidmvlelem1  47424