Theorem ss2rabdv 4023

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ral 3078  df-rab 3414  df-ss 3916

This theorem is used by:  ss2rabi  4024  rabssrabd  4031  sess1  5616  suppssov1  8198  suppssov2  8199  suppssfv  8203  cofon1  8665  naddssim  8679  harword  9541  rankval4b  9861  scottex  9914  scottexOLD  9915  mrcss  17770  mndpsuppss  18939  ablfac1b  20266  mptscmfsupp0  21182  lspss  21239  dsmmacl  22027  dsmmsubg  22029  dsmmlss  22030  aspss  22164  psdmul  22467  scmatdmat  22810  clsss  23352  lfinpfin  23823  qustgpopn  24419  metss2lem  24810  equivcau  25601  rrxmvallem  25705  ovolsslem  25785  itg2monolem1  26051  lgamucov  27347  sqff1o  27491  musum  27500  nna4b4nsq  27972  madess  28234  cofcut1  28288  bdayons  28644  cusgrfilem1  30018  clwlknf1oclwwlknlem3  30656  occon  31871  spanss  31932  rmfsupp2  33780  fldgenss  33860  evlextv  34156  locfinreflem  34454  omsmon  34913  orvclteinc  35091  fin2solem  38497  poimirlem26  38532  poimirlem27  38533  cnambfre  38554  pmaple  40786  pclssN  40919  2polssN  40940  dihglblem3N  42320  dochss  42390  mapdordlem2  42662  itgoss  44123  nzss  45260  ovnsslelem  47514  gpgusgralem  49098  rmsuppss  49426  scmsuppss  49427