Theorem ss2rabdv 4031

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  {crab 3417   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ral 3080  df-rab 3418  df-ss 3924

This theorem is referenced by:  ss2rabi  4032  rabssrabd  4039  sess1  5616  suppssov1  8181  suppssov2  8182  suppssfv  8186  cofon1  8646  naddssim  8660  harword  9513  scottex  9847  mrcss  17660  mndpsuppss  18811  ablfac1b  20130  mptscmfsupp0  21014  lspss  21071  dsmmacl  21848  dsmmsubg  21850  dsmmlss  21851  aspss  21983  psdmul  22286  scmatdmat  22629  clsss  23168  lfinpfin  23638  qustgpopn  24234  metss2lem  24625  equivcau  25416  rrxmvallem  25520  ovolsslem  25600  itg2monolem1  25866  lgamucov  27156  sqff1o  27300  musum  27309  madess  28013  cofcut1  28067  bdayons  28423  cusgrfilem1  29710  clwlknf1oclwwlknlem3  30339  occon  31544  spanss  31605  rmfsupp2  33465  fldgenss  33547  evlextv  33844  locfinreflem  34142  omsmon  34600  orvclteinc  34778  rankval4b  35403  fin2solem  38112  poimirlem26  38152  poimirlem27  38153  cnambfre  38174  pmaple  40392  pclssN  40525  2polssN  40546  dihglblem3N  41926  dochss  41996  mapdordlem2  42268  nna4b4nsq  43249  itgoss  43747  nzss  44886  ovnsslelem  47133  gpgusgralem  48677  rmsuppss  49002  scmsuppss  49003