Theorem ss2rabdv 4032

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  {crab 3419   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ral 3083  df-rab 3420  df-ss 3925

This theorem is used by:  ss2rabi  4033  rabssrabd  4040  sess1  5631  suppssov1  8202  suppssov2  8203  suppssfv  8207  cofon1  8667  naddssim  8681  harword  9535  scottex  9872  scottexOLD  9873  mrcss  17697  mndpsuppss  18854  ablfac1b  20173  mptscmfsupp0  21085  lspss  21142  dsmmacl  21928  dsmmsubg  21930  dsmmlss  21931  aspss  22063  psdmul  22366  scmatdmat  22709  clsss  23248  lfinpfin  23718  qustgpopn  24314  metss2lem  24705  equivcau  25496  rrxmvallem  25600  ovolsslem  25680  itg2monolem1  25946  lgamucov  27239  sqff1o  27383  musum  27392  madess  28096  cofcut1  28150  bdayons  28506  cusgrfilem1  29842  clwlknf1oclwwlknlem3  30471  occon  31676  spanss  31737  rmfsupp2  33588  fldgenss  33668  evlextv  33963  locfinreflem  34261  omsmon  34720  orvclteinc  34898  rankval4b  35518  fin2solem  38298  poimirlem26  38338  poimirlem27  38339  cnambfre  38360  pmaple  40576  pclssN  40709  2polssN  40730  dihglblem3N  42110  dochss  42180  mapdordlem2  42452  nna4b4nsq  43433  itgoss  43931  nzss  45068  ovnsslelem  47315  gpgusgralem  48862  rmsuppss  49191  scmsuppss  49192