Theorem ss2rabdv 4027

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-rab 3400  df-ss 3918

This theorem is referenced by:  ss2rabi  4028  rabssrabd  4035  sess1  5589  suppssov1  8139  suppssov2  8140  suppssfv  8144  cofon1  8600  naddssim  8613  harword  9468  scottex  9797  mrcss  17539  mndpsuppss  18690  ablfac1b  20001  mptscmfsupp0  20878  lspss  20935  dsmmacl  21696  dsmmsubg  21698  dsmmlss  21699  aspss  21832  psdmul  22109  scmatdmat  22459  clsss  22998  lfinpfin  23468  qustgpopn  24064  metss2lem  24455  equivcau  25256  rrxmvallem  25360  ovolsslem  25441  itg2monolem1  25707  lgamucov  27004  sqff1o  27148  musum  27157  madess  27862  cofcut1  27916  bdayons  28272  cusgrfilem1  29529  clwlknf1oclwwlknlem3  30158  occon  31362  spanss  31423  rmfsupp2  33320  fldgenss  33398  evlextv  33707  locfinreflem  33997  omsmon  34455  orvclteinc  34633  rankval4b  35256  fin2solem  37807  poimirlem26  37847  poimirlem27  37848  cnambfre  37869  pmaple  40021  pclssN  40154  2polssN  40175  dihglblem3N  41555  dochss  41625  mapdordlem2  41897  nna4b4nsq  42903  itgoss  43405  nzss  44558  ovnsslelem  46804  gpgusgralem  48302  rmsuppss  48616  scmsuppss  48617