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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  {crab 3414   ⊆ wss 3902

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 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ral 3079  df-rab 3415  df-ss 3919

This theorem is used by:  ss2rabi  4027  rabssrabd  4034  sess1  5624  suppssov1  8199  suppssov2  8200  suppssfv  8204  cofon1  8664  naddssim  8678  harword  9539  scottex  9876  scottexOLD  9877  mrcss  17710  mndpsuppss  18878  ablfac1b  20205  mptscmfsupp0  21117  lspss  21174  dsmmacl  21960  dsmmsubg  21962  dsmmlss  21963  aspss  22097  psdmul  22400  scmatdmat  22743  clsss  23285  lfinpfin  23756  qustgpopn  24352  metss2lem  24743  equivcau  25534  rrxmvallem  25638  ovolsslem  25718  itg2monolem1  25984  lgamucov  27282  sqff1o  27426  musum  27435  madess  28139  cofcut1  28193  bdayons  28549  cusgrfilem1  29923  clwlknf1oclwwlknlem3  30561  occon  31776  spanss  31837  rmfsupp2  33685  fldgenss  33765  evlextv  34060  locfinreflem  34358  omsmon  34817  orvclteinc  34995  rankval4b  35615  fin2solem  38368  poimirlem26  38403  poimirlem27  38404  cnambfre  38425  pmaple  40642  pclssN  40775  2polssN  40796  dihglblem3N  42176  dochss  42246  mapdordlem2  42518  nna4b4nsq  43514  itgoss  44012  nzss  45149  ovnsslelem  47396  gpgusgralem  48980  rmsuppss  49308  scmsuppss  49309