Theorem ss2rabdv 4016

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 4013	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

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

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 3391  df-ss 3907

This theorem is referenced by:  ss2rabi  4017  rabssrabd  4024  sess1  5589  suppssov1  8140  suppssov2  8141  suppssfv  8145  cofon1  8601  naddssim  8614  harword  9471  scottex  9800  mrcss  17573  mndpsuppss  18724  ablfac1b  20038  mptscmfsupp0  20913  lspss  20970  dsmmacl  21731  dsmmsubg  21733  dsmmlss  21734  aspss  21866  psdmul  22142  scmatdmat  22490  clsss  23029  lfinpfin  23499  qustgpopn  24095  metss2lem  24486  equivcau  25277  rrxmvallem  25381  ovolsslem  25461  itg2monolem1  25727  lgamucov  27015  sqff1o  27159  musum  27168  madess  27872  cofcut1  27926  bdayons  28282  cusgrfilem1  29539  clwlknf1oclwwlknlem3  30168  occon  31373  spanss  31434  rmfsupp2  33314  fldgenss  33392  evlextv  33701  locfinreflem  34000  omsmon  34458  orvclteinc  34636  rankval4b  35259  fin2solem  37941  poimirlem26  37981  poimirlem27  37982  cnambfre  38003  pmaple  40221  pclssN  40354  2polssN  40375  dihglblem3N  41755  dochss  41825  mapdordlem2  42097  nna4b4nsq  43107  itgoss  43609  nzss  44762  ovnsslelem  47006  gpgusgralem  48544  rmsuppss  48858  scmsuppss  48859