Theorem abssdv 4041

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

Syntax hints:   → wi 4   ∈ wcel 2107  {cab 2712   ⊆ wss 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ss 3941

This theorem is referenced by:  dfopif  4843  opabssxpd  5698  fmpt  7096  fabexd  7927  eroprf  8823  cfslb2n  10274  rankcf  10783  genpv  11005  genpdm  11008  fimaxre3  12180  supadd  12202  supmul  12206  hashf1lem2  14462  mertenslem2  15888  4sqlem11  16960  lss1d  20905  lspsn  20944  lpval  23062  lpsscls  23064  ptuni2  23499  ptbasfi  23504  prdstopn  23551  xkopt  23578  tgpconncompeqg  24035  metrest  24448  mbfeqalem1  25579  limcfval  25810  nosupno  27651  nosupbday  27653  noinfno  27666  noinfbday  27668  addsproplem2  27906  addsuniflem  27937  addsbdaylem  27952  negsid  27976  mulsproplem9  28053  ssltmul1  28076  ssltmul2  28077  precsexlem8  28141  precsexlem11  28144  onaddscl  28189  onmulscl  28190  recut  28331  0reno  28332  nmosetre  30677  nmopsetretALT  31776  nmfnsetre  31790  sigaclcuni  34057  bnj849  34877  deranglem  35109  derangsn  35113  liness  36084  mblfinlem3  37604  ismblfin  37606  itg2addnclem  37616  areacirclem2  37654  sdclem2  37687  sdclem1  37688  ismtyval  37745  heibor1lem  37754  heibor1  37755  pmapglbx  39709  eldiophb  42705  hbtlem2  43073  oaun3lem1  43323  oaun3lem2  43324  upbdrech  45261