Theorem abssdv 4066

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

Syntax hints:   → wi 4   ∈ wcel 2107  {cab 2710   ⊆ wss 3949

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 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  dfopif  4871  opabssxpd  5724  fmpt  7110  eroprf  8809  cfslb2n  10263  rankcf  10772  genpv  10994  genpdm  10997  fimaxre3  12160  supadd  12182  supmul  12186  hashfacenOLD  14414  hashf1lem1OLD  14416  hashf1lem2  14417  mertenslem2  15831  4sqlem11  16888  lss1d  20574  lspsn  20613  lpval  22643  lpsscls  22645  ptuni2  23080  ptbasfi  23085  prdstopn  23132  xkopt  23159  tgpconncompeqg  23616  metrest  24033  mbfeqalem1  25158  limcfval  25389  nosupno  27206  nosupbday  27208  noinfno  27221  noinfbday  27223  addsproplem2  27454  addsuniflem  27484  negsid  27515  mulsproplem9  27580  ssltmul1  27602  ssltmul2  27603  precsexlem8  27660  precsexlem11  27663  nmosetre  30017  nmopsetretALT  31116  nmfnsetre  31130  sigaclcuni  33116  bnj849  33936  deranglem  34157  derangsn  34161  liness  35117  mblfinlem3  36527  ismblfin  36529  itg2addnclem  36539  areacirclem2  36577  sdclem2  36610  sdclem1  36611  ismtyval  36668  heibor1lem  36677  heibor1  36678  pmapglbx  38640  eldiophb  41495  hbtlem2  41866  oaun3lem1  42124  oaun3lem2  42125  upbdrech  44015