Theorem ss2rabdv 4026

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  {crab 3413   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ral 3076  df-rab 3414  df-ss 3919

This theorem is referenced by:  ss2rabi  4027  rabssrabd  4034  sess1  5608  suppssov1  8170  suppssov2  8171  suppssfv  8175  cofon1  8635  naddssim  8649  harword  9504  scottex  9836  mrcss  17638  mndpsuppss  18789  ablfac1b  20102  mptscmfsupp0  20981  lspss  21038  dsmmacl  21780  dsmmsubg  21782  dsmmlss  21783  aspss  21915  psdmul  22218  scmatdmat  22562  clsss  23101  lfinpfin  23571  qustgpopn  24167  metss2lem  24558  equivcau  25349  rrxmvallem  25453  ovolsslem  25533  itg2monolem1  25799  lgamucov  27089  sqff1o  27233  musum  27242  madess  27946  cofcut1  28000  bdayons  28356  cusgrfilem1  29612  clwlknf1oclwwlknlem3  30241  occon  31446  spanss  31507  rmfsupp2  33378  fldgenss  33463  evlextv  33799  locfinreflem  34097  omsmon  34555  orvclteinc  34733  rankval4b  35356  fin2solem  38065  poimirlem26  38105  poimirlem27  38106  cnambfre  38127  pmaple  40345  pclssN  40478  2polssN  40499  dihglblem3N  41879  dochss  41949  mapdordlem2  42221  nna4b4nsq  43202  itgoss  43700  nzss  44853  ovnsslelem  47094  gpgusgralem  48638  rmsuppss  48952  scmsuppss  48953