Theorem abssdv 4028

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2707   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3928

This theorem is referenced by:  dfopif  4830  opabssxpd  5678  fmpt  7064  fabexd  7893  eroprf  8765  cfslb2n  10197  rankcf  10706  genpv  10928  genpdm  10931  fimaxre3  12105  supadd  12127  supmul  12131  hashf1lem2  14397  mertenslem2  15827  4sqlem11  16902  lss1d  20901  lspsn  20940  lpval  23059  lpsscls  23061  ptuni2  23496  ptbasfi  23501  prdstopn  23548  xkopt  23575  tgpconncompeqg  24032  metrest  24445  mbfeqalem1  25575  limcfval  25806  nosupno  27648  nosupbday  27650  noinfno  27663  noinfbday  27665  addsproplem2  27917  addsuniflem  27948  addsbdaylem  27963  negsid  27987  mulsproplem9  28067  ssltmul1  28090  ssltmul2  28091  precsexlem8  28156  precsexlem11  28159  onaddscl  28214  onmulscl  28215  recut  28400  0reno  28401  nmosetre  30743  nmopsetretALT  31842  nmfnsetre  31856  sigaclcuni  34101  bnj849  34908  deranglem  35146  derangsn  35150  liness  36126  mblfinlem3  37646  ismblfin  37648  itg2addnclem  37658  areacirclem2  37696  sdclem2  37729  sdclem1  37730  ismtyval  37787  heibor1lem  37796  heibor1  37797  pmapglbx  39756  eldiophb  42738  hbtlem2  43106  oaun3lem1  43356  oaun3lem2  43357  upbdrech  45296