Theorem ss2rabdv 4024

Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.) Avoid axioms. (Revised by TM, 1-Feb-2026.)

Hypothesis

Ref	Expression
ss2rabdv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ss2rabdv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ss2rabdv

Step	Hyp	Ref	Expression
1		ss2rabdv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ralrimiva 3125	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
3	2	ss2rabd 4021	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  {crab 3396   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-ral 3049  df-rab 3397  df-ss 3915

This theorem is referenced by:  ss2rabi  4025  rabssrabd  4032  sess1  5586  suppssov1  8135  suppssov2  8136  suppssfv  8140  cofon1  8595  naddssim  8608  harword  9458  scottex  9787  mrcss  17526  mndpsuppss  18677  ablfac1b  19988  mptscmfsupp0  20864  lspss  20921  dsmmacl  21682  dsmmsubg  21684  dsmmlss  21685  aspss  21818  psdmul  22084  scmatdmat  22433  clsss  22972  lfinpfin  23442  qustgpopn  24038  metss2lem  24429  equivcau  25230  rrxmvallem  25334  ovolsslem  25415  itg2monolem1  25681  lgamucov  26978  sqff1o  27122  musum  27131  madess  27824  cofcut1  27867  bdayon  28212  cusgrfilem1  29438  clwlknf1oclwwlknlem3  30067  occon  31271  spanss  31332  rmfsupp2  33214  fldgenss  33291  locfinreflem  33876  omsmon  34334  orvclteinc  34512  rankval4b  35134  fin2solem  37669  poimirlem26  37709  poimirlem27  37710  cnambfre  37731  pmaple  39883  pclssN  40016  2polssN  40037  dihglblem3N  41417  dochss  41487  mapdordlem2  41759  nna4b4nsq  42781  itgoss  43283  nzss  44437  ovnsslelem  46685  gpgusgralem  48183  rmsuppss  48497  scmsuppss  48498