Theorem ss2rabdv 4013

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  {crab 3392   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ral 3055  df-rab 3393  df-ss 3907

This theorem is referenced by:  ss2rabi  4014  rabssrabd  4021  sess1  5590  suppssov1  8144  suppssov2  8145  suppssfv  8149  cofon1  8605  naddssim  8618  harword  9475  scottex  9807  mrcss  17580  mndpsuppss  18731  ablfac1b  20045  mptscmfsupp0  20924  lspss  20981  dsmmacl  21723  dsmmsubg  21725  dsmmlss  21726  aspss  21858  psdmul  22161  scmatdmat  22505  clsss  23044  lfinpfin  23514  qustgpopn  24110  metss2lem  24501  equivcau  25292  rrxmvallem  25396  ovolsslem  25476  itg2monolem1  25742  lgamucov  27026  sqff1o  27170  musum  27179  madess  27883  cofcut1  27937  bdayons  28293  cusgrfilem1  29549  clwlknf1oclwwlknlem3  30178  occon  31383  spanss  31444  rmfsupp2  33326  fldgenss  33407  evlextv  33733  locfinreflem  34031  omsmon  34489  orvclteinc  34667  rankval4b  35288  fin2solem  37980  poimirlem26  38020  poimirlem27  38021  cnambfre  38042  pmaple  40260  pclssN  40393  2polssN  40414  dihglblem3N  41794  dochss  41864  mapdordlem2  42136  nna4b4nsq  43117  itgoss  43615  nzss  44768  ovnsslelem  47010  gpgusgralem  48554  rmsuppss  48868  scmsuppss  48869