Theorem ss2rabdv 4000

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  {crab 3412   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-rab 3413  df-ss 3896

This theorem is used by:  ss2rabi  4001  rabssrabd  4008  sess1  5615  suppssov1  8217  suppssov2  8218  suppssfv  8222  cofon1  8684  naddssim  8698  harword  9560  rankval4b  9883  scottex  9936  scottexOLD  9937  mrcss  17795  mndpsuppss  18964  ablfac1b  20291  mptscmfsupp0  21207  lspss  21264  dsmmacl  22052  dsmmsubg  22054  dsmmlss  22055  aspss  22189  psdmul  22492  scmatdmat  22835  clsss  23377  lfinpfin  23848  qustgpopn  24444  metss2lem  24835  equivcau  25626  rrxmvallem  25730  ovolsslem  25810  itg2monolem1  26076  lgamucov  27370  sqff1o  27514  musum  27523  madess  28257  cofcut1  28311  bdayons  28667  cusgrfilem1  30041  clwlknf1oclwwlknlem3  30679  occon  31894  spanss  31955  rmfsupp2  33844  fldgenss  33924  evlextv  34220  locfinreflem  34518  omsmon  34976  orvclteinc  35154  fin2solem  38622  poimirlem26  38657  poimirlem27  38658  cnambfre  38679  pmaple  40911  pclssN  41044  2polssN  41065  dihglblem3N  42445  dochss  42515  mapdordlem2  42787  itgoss  44258  nzss  45394  ovnsslelem  47663  gpgusgralem  49247  rmsuppss  49575  scmsuppss  49576