Theorem ss2rabdv 4030

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  {crab 3416   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-rab 3417  df-ss 3923

This theorem is referenced by:  ss2rabi  4031  rabssrabd  4038  sess1  5628  suppssov1  8194  suppssov2  8195  suppssfv  8199  cofon1  8659  naddssim  8673  harword  9526  scottex  9860  mrcss  17673  mndpsuppss  18824  ablfac1b  20143  mptscmfsupp0  21029  lspss  21086  dsmmacl  21872  dsmmsubg  21874  dsmmlss  21875  aspss  22007  psdmul  22310  scmatdmat  22653  clsss  23192  lfinpfin  23662  qustgpopn  24258  metss2lem  24649  equivcau  25440  rrxmvallem  25544  ovolsslem  25624  itg2monolem1  25890  lgamucov  27183  sqff1o  27327  musum  27336  madess  28040  cofcut1  28094  bdayons  28450  cusgrfilem1  29786  clwlknf1oclwwlknlem3  30415  occon  31620  spanss  31681  rmfsupp2  33538  fldgenss  33618  evlextv  33913  locfinreflem  34211  omsmon  34669  orvclteinc  34847  rankval4b  35474  fin2solem  38238  poimirlem26  38278  poimirlem27  38279  cnambfre  38300  pmaple  40516  pclssN  40649  2polssN  40670  dihglblem3N  42050  dochss  42120  mapdordlem2  42392  nna4b4nsq  43375  itgoss  43873  nzss  45010  ovnsslelem  47257  gpgusgralem  48804  rmsuppss  49133  scmsuppss  49134