Theorem ss2rabdv 4029

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 3130	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
3	2	ss2rabd 4026	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  {crab 3401   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rab 3402  df-ss 3920

This theorem is referenced by:  ss2rabi  4030  rabssrabd  4037  sess1  5597  suppssov1  8149  suppssov2  8150  suppssfv  8154  cofon1  8610  naddssim  8623  harword  9480  scottex  9809  mrcss  17551  mndpsuppss  18702  ablfac1b  20013  mptscmfsupp0  20890  lspss  20947  dsmmacl  21708  dsmmsubg  21710  dsmmlss  21711  aspss  21844  psdmul  22121  scmatdmat  22471  clsss  23010  lfinpfin  23480  qustgpopn  24076  metss2lem  24467  equivcau  25268  rrxmvallem  25372  ovolsslem  25453  itg2monolem1  25719  lgamucov  27016  sqff1o  27160  musum  27169  madess  27874  cofcut1  27928  bdayons  28284  cusgrfilem1  29541  clwlknf1oclwwlknlem3  30170  occon  31374  spanss  31435  rmfsupp2  33331  fldgenss  33409  evlextv  33718  locfinreflem  34017  omsmon  34475  orvclteinc  34653  rankval4b  35275  fin2solem  37854  poimirlem26  37894  poimirlem27  37895  cnambfre  37916  pmaple  40134  pclssN  40267  2polssN  40288  dihglblem3N  41668  dochss  41738  mapdordlem2  42010  nna4b4nsq  43015  itgoss  43517  nzss  44670  ovnsslelem  46915  gpgusgralem  48413  rmsuppss  48727  scmsuppss  48728