Theorem ss2rabdv 4015

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ral 3052  df-rab 3390  df-ss 3906

This theorem is referenced by:  ss2rabi  4016  rabssrabd  4023  sess1  5596  suppssov1  8147  suppssov2  8148  suppssfv  8152  cofon1  8608  naddssim  8621  harword  9478  scottex  9809  mrcss  17582  mndpsuppss  18733  ablfac1b  20047  mptscmfsupp0  20922  lspss  20979  dsmmacl  21721  dsmmsubg  21723  dsmmlss  21724  aspss  21856  psdmul  22132  scmatdmat  22480  clsss  23019  lfinpfin  23489  qustgpopn  24085  metss2lem  24476  equivcau  25267  rrxmvallem  25371  ovolsslem  25451  itg2monolem1  25717  lgamucov  27001  sqff1o  27145  musum  27154  madess  27858  cofcut1  27912  bdayons  28268  cusgrfilem1  29524  clwlknf1oclwwlknlem3  30153  occon  31358  spanss  31419  rmfsupp2  33299  fldgenss  33377  evlextv  33686  locfinreflem  33984  omsmon  34442  orvclteinc  34620  rankval4b  35243  fin2solem  37927  poimirlem26  37967  poimirlem27  37968  cnambfre  37989  pmaple  40207  pclssN  40340  2polssN  40361  dihglblem3N  41741  dochss  41811  mapdordlem2  42083  nna4b4nsq  43093  itgoss  43591  nzss  44744  ovnsslelem  46988  gpgusgralem  48532  rmsuppss  48846  scmsuppss  48847