Theorem ss2rabdv 4005

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063  {crab 3067   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rabssrabd  4012  sess1  5548  suppssov1  7985  suppssfv  7989  harword  9252  mrcss  17242  ablfac1b  19588  mptscmfsupp0  20103  lspss  20161  dsmmacl  20858  dsmmsubg  20860  dsmmlss  20861  aspss  20991  scmatdmat  21572  clsss  22113  lfinpfin  22583  qustgpopn  23179  metss2lem  23573  equivcau  24369  rrxmvallem  24473  ovolsslem  24553  itg2monolem1  24820  lgamucov  26092  sqff1o  26236  musum  26245  cusgrfilem1  27725  clwlknf1oclwwlknlem3  28348  rmfsupp2  31394  locfinreflem  31692  omsmon  32165  orvclteinc  32342  naddssim  33764  madess  33986  cofcut1  34017  fin2solem  35690  poimirlem26  35730  poimirlem27  35731  cnambfre  35752  pclssN  37835  2polssN  37856  dihglblem3N  39236  dochss  39306  mapdordlem2  39578  nna4b4nsq  40413  nzss  41824  rmsuppss  45594  mndpsuppss  45595  scmsuppss  45596