Theorem ss2rabdv 4009

Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)

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 3103	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
3		ss2rab 4004	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒} ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4	2, 3	sylibr 233	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ⊆ {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064  {crab 3068   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  rabssrabd  4016  sess1  5557  suppssov1  8014  suppssfv  8018  harword  9322  mrcss  17325  ablfac1b  19673  mptscmfsupp0  20188  lspss  20246  dsmmacl  20948  dsmmsubg  20950  dsmmlss  20951  aspss  21081  scmatdmat  21664  clsss  22205  lfinpfin  22675  qustgpopn  23271  metss2lem  23667  equivcau  24464  rrxmvallem  24568  ovolsslem  24648  itg2monolem1  24915  lgamucov  26187  sqff1o  26331  musum  26340  cusgrfilem1  27822  clwlknf1oclwwlknlem3  28447  rmfsupp2  31492  locfinreflem  31790  omsmon  32265  orvclteinc  32442  naddssim  33837  madess  34059  cofcut1  34090  fin2solem  35763  poimirlem26  35803  poimirlem27  35804  cnambfre  35825  pclssN  37908  2polssN  37929  dihglblem3N  39309  dochss  39379  mapdordlem2  39651  nna4b4nsq  40497  nzss  41935  rmsuppss  45706  mndpsuppss  45707  scmsuppss  45708