Theorem ss2rabdv 4003

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  {crab 3416   ⊆ wss 3900

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rab 3417  df-ss 3901

This theorem is used by:  ss2rabi  4004  rabssrabd  4011  sess1  5621  suppssov1  8245  suppssov2  8246  suppssfv  8250  cofon1  8712  naddssim  8726  harword  9587  rankval4b  9910  scottex  9963  scottexOLD  9964  mrcss  17822  mndpsuppss  18991  ablfac1b  20319  mptscmfsupp0  21235  lspss  21292  dsmmacl  22080  dsmmsubg  22082  dsmmlss  22083  aspss  22217  psdmul  22520  scmatdmat  22863  clsss  23405  lfinpfin  23876  qustgpopn  24472  metss2lem  24863  equivcau  25654  rrxmvallem  25758  ovolsslem  25838  itg2monolem1  26104  lgamucov  27398  sqff1o  27542  musum  27551  madess  28285  cofcut1  28339  bdayons  28695  cusgrfilem1  30069  clwlknf1oclwwlknlem3  30707  occon  31922  spanss  31983  rmfsupp2  33874  fldgenss  33962  evlextv  34257  locfinreflem  34555  omsmon  35013  orvclteinc  35191  fin2solem  38734  poimirlem26  38769  poimirlem27  38770  cnambfre  38791  pmaple  41021  pclssN  41154  2polssN  41175  dihglblem3N  42555  dochss  42625  mapdordlem2  42897  itgoss  44368  nzss  45504  ovnsslelem  47785  gpgusgralem  49369  rmsuppss  49697  scmsuppss  49698