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 2897	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
4	2, 3	sseqtrrdi 3972	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {cab 2739   ⊆ 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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916

This theorem is used by:  dfopif  4830  abexd  5287  opabssxpd  5698  fmpt  7110  fabexd  7949  eroprf  8836  cfslb2n  10346  axdc2lem  10526  rankcf  10862  genpv  11084  genpdm  11087  fimaxre3  12263  supadd  12285  supmul  12289  hashf1lem2  14601  mertenslem2  16054  4sqlem11  17133  lss1d  21238  lspsn  21277  lpval  23457  lpsscls  23459  ptuni2  23895  ptbasfi  23900  prdstopn  23947  xkopt  23974  tgpconncompeqg  24431  metrest  24843  mbfeqalem1  25962  limcfval  26192  nosupno  28060  nosupbday  28062  noinfno  28075  noinfbday  28077  addsproplem2  28356  addsuniflem  28387  addbdaylem  28403  negsid  28427  mulsproplem9  28510  sltmuls1  28533  sltmuls2  28534  precsexlem8  28600  precsexlem11  28603  onaddscl  28663  onmulscl  28664  recut  28880  elreno2  28881  nmosetre  31366  nmopsetretALT  32465  nmfnsetre  32479  sigaclcuni  34750  bnj849  35555  vonf1oonfo  35898  deranglem  35931  derangsn  35935  liness  36910  nmulprop  36939  mblfinlem3  38577  ismblfin  38579  itg2addnclem  38589  areacirclem2  38627  sdclem2  38676  sdclem1  38677  ismtyval  38734  heibor1lem  38743  heibor1  38744  pmapglbx  40826  eldiophb  43767  hbtlem2  44125  oaun3lem1  44375  oaun3lem2  44376  upbdrech  46320  hoidmvlelem1  47604