Theorem abssdv 3994

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {cab 2741   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3900

This theorem is used by:  dfopif  4839  abexd  5290  opabssxpd  5701  fmpt  7118  fabexd  7956  eroprf  8847  cfslb2n  10356  axdc2lem  10536  rankcf  10872  genpv  11094  genpdm  11097  fimaxre3  12273  supadd  12295  supmul  12299  hashf1lem2  14611  mertenslem2  16066  4sqlem11  17145  lss1d  21250  lspsn  21289  lpval  23469  lpsscls  23471  ptuni2  23907  ptbasfi  23912  prdstopn  23959  xkopt  23986  tgpconncompeqg  24443  metrest  24855  mbfeqalem1  25974  limcfval  26204  nosupno  28072  nosupbday  28074  noinfno  28087  noinfbday  28089  addsproplem2  28368  addsuniflem  28399  addbdaylem  28415  negsid  28439  mulsproplem9  28522  sltmuls1  28545  sltmuls2  28546  precsexlem8  28612  precsexlem11  28615  onaddscl  28675  onmulscl  28676  recut  28892  elreno2  28893  nmosetre  31378  nmopsetretALT  32477  nmfnsetre  32491  sigaclcuni  34803  bnj849  35608  vonf1oonfo  36003  deranglem  36052  derangsn  36056  liness  37037  nmulprop  37066  mblfinlem3  38717  ismblfin  38719  itg2addnclem  38729  areacirclem2  38767  sdclem2  38816  sdclem1  38817  ismtyval  38874  heibor1lem  38883  heibor1  38884  pmapglbx  40966  eldiophb  43908  hbtlem2  44266  oaun3lem1  44516  oaun3lem2  44517  upbdrech  46460  hoidmvlelem1  47744