Theorem ss2rabdv 4029

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044  {crab 3396   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rab 3397  df-ss 3922

This theorem is referenced by:  rabssrabd  4036  sess1  5588  suppssov1  8137  suppssov2  8138  suppssfv  8142  cofon1  8597  naddssim  8610  harword  9474  scottex  9800  mrcss  17540  mndpsuppss  18657  ablfac1b  19969  mptscmfsupp0  20848  lspss  20905  dsmmacl  21666  dsmmsubg  21668  dsmmlss  21669  aspss  21802  psdmul  22069  scmatdmat  22418  clsss  22957  lfinpfin  23427  qustgpopn  24023  metss2lem  24415  equivcau  25216  rrxmvallem  25320  ovolsslem  25401  itg2monolem1  25667  lgamucov  26964  sqff1o  27108  musum  27117  madess  27808  cofcut1  27851  bdayon  28196  cusgrfilem1  29419  clwlknf1oclwwlknlem3  30045  occon  31249  spanss  31310  rmfsupp2  33191  fldgenss  33268  locfinreflem  33809  omsmon  34268  orvclteinc  34446  fin2solem  37588  poimirlem26  37628  poimirlem27  37629  cnambfre  37650  pclssN  39876  2polssN  39897  dihglblem3N  41277  dochss  41347  mapdordlem2  41619  nna4b4nsq  42636  itgoss  43139  nzss  44293  ovnsslelem  46545  gpgusgralem  48044  rmsuppss  48358  scmsuppss  48359