Theorem abssdv 4019

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cab 2714   ⊆ wss 3901

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918

This theorem is referenced by:  dfopif  4826  abexd  5270  opabssxpd  5671  fmpt  7055  fabexd  7879  eroprf  8752  cfslb2n  10178  axdc2lem  10358  rankcf  10688  genpv  10910  genpdm  10913  fimaxre3  12088  supadd  12110  supmul  12114  hashf1lem2  14379  mertenslem2  15808  4sqlem11  16883  lss1d  20914  lspsn  20953  lpval  23083  lpsscls  23085  ptuni2  23520  ptbasfi  23525  prdstopn  23572  xkopt  23599  tgpconncompeqg  24056  metrest  24468  mbfeqalem1  25598  limcfval  25829  nosupno  27671  nosupbday  27673  noinfno  27686  noinfbday  27688  addsproplem2  27966  addsuniflem  27997  addbdaylem  28013  negsid  28037  mulsproplem9  28120  sltmuls1  28143  sltmuls2  28144  precsexlem8  28210  precsexlem11  28213  onaddscl  28273  onmulscl  28274  recut  28490  elreno2  28491  nmosetre  30839  nmopsetretALT  31938  nmfnsetre  31952  sigaclcuni  34275  bnj849  35081  deranglem  35360  derangsn  35364  liness  36339  mblfinlem3  37860  ismblfin  37862  itg2addnclem  37872  areacirclem2  37910  sdclem2  37943  sdclem1  37944  ismtyval  38001  heibor1lem  38010  heibor1  38011  pmapglbx  40039  eldiophb  43009  hbtlem2  43376  oaun3lem1  43626  oaun3lem2  43627  upbdrech  45563  hoidmvlelem1  46849