Theorem abssdv 4021

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

Syntax hints:   → wi 4   ∈ wcel 2143  {cab 2741   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922

This theorem is referenced by:  dfopif  4835  abexd  5296  opabssxpd  5708  fmpt  7105  fabexd  7930  eroprf  8809  cfslb2n  10247  axdc2lem  10427  rankcf  10757  genpv  10979  genpdm  10982  fimaxre3  12156  supadd  12178  supmul  12182  hashf1lem2  14489  mertenslem2  15935  4sqlem11  17010  lss1d  21084  lspsn  21123  lpval  23296  lpsscls  23298  ptuni2  23733  ptbasfi  23738  prdstopn  23785  xkopt  23812  tgpconncompeqg  24269  metrest  24681  mbfeqalem1  25800  limcfval  26031  nosupno  27867  nosupbday  27869  noinfno  27882  noinfbday  27884  addsproplem2  28163  addsuniflem  28194  addbdaylem  28210  negsid  28234  mulsproplem9  28317  sltmuls1  28340  sltmuls2  28341  precsexlem8  28407  precsexlem11  28410  onaddscl  28470  onmulscl  28471  recut  28687  elreno2  28688  nmosetre  31116  nmopsetretALT  32215  nmfnsetre  32229  sigaclcuni  34508  bnj849  35313  vonf1oonfo  35599  deranglem  35658  derangsn  35662  liness  36637  nmulprop  36682  mblfinlem3  38330  ismblfin  38332  itg2addnclem  38342  areacirclem2  38380  sdclem2  38413  sdclem1  38414  ismtyval  38471  heibor1lem  38480  heibor1  38481  pmapglbx  40563  eldiophb  43508  hbtlem2  43871  oaun3lem1  44121  oaun3lem2  44122  upbdrech  46044  hoidmvlelem1  47329