Theorem abssdv 4014

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

Syntax hints:   → wi 4   ∈ wcel 2111  {cab 2709   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ss 3914

This theorem is referenced by:  dfopif  4819  opabssxpd  5661  fmpt  7043  fabexd  7867  eroprf  8739  cfslb2n  10159  rankcf  10668  genpv  10890  genpdm  10893  fimaxre3  12068  supadd  12090  supmul  12094  hashf1lem2  14363  mertenslem2  15792  4sqlem11  16867  lss1d  20896  lspsn  20935  lpval  23054  lpsscls  23056  ptuni2  23491  ptbasfi  23496  prdstopn  23543  xkopt  23570  tgpconncompeqg  24027  metrest  24439  mbfeqalem1  25569  limcfval  25800  nosupno  27642  nosupbday  27644  noinfno  27657  noinfbday  27659  addsproplem2  27913  addsuniflem  27944  addsbdaylem  27959  negsid  27983  mulsproplem9  28063  ssltmul1  28086  ssltmul2  28087  precsexlem8  28152  precsexlem11  28155  onaddscl  28210  onmulscl  28211  recut  28398  0reno  28399  nmosetre  30744  nmopsetretALT  31843  nmfnsetre  31857  sigaclcuni  34131  bnj849  34937  deranglem  35210  derangsn  35214  liness  36189  mblfinlem3  37709  ismblfin  37711  itg2addnclem  37721  areacirclem2  37759  sdclem2  37792  sdclem1  37793  ismtyval  37850  heibor1lem  37859  heibor1  37860  pmapglbx  39878  eldiophb  42860  hbtlem2  43227  oaun3lem1  43477  oaun3lem2  43478  upbdrech  45416