Theorem ss2rabdv 4071

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∀wral 3058  {crab 3429   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rab 3430  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  rabssrabd  4079  sess1  5646  suppssov1  8203  suppssov2  8204  suppssfv  8208  cofon1  8693  naddssim  8706  harword  9587  scottex  9909  mrcss  17596  ablfac1b  20027  mptscmfsupp0  20810  lspss  20868  dsmmacl  21675  dsmmsubg  21677  dsmmlss  21678  aspss  21810  psdmul  22090  scmatdmat  22430  clsss  22971  lfinpfin  23441  qustgpopn  24037  metss2lem  24433  equivcau  25241  rrxmvallem  25345  ovolsslem  25426  itg2monolem1  25693  lgamucov  26983  sqff1o  27127  musum  27136  madess  27816  cofcut1  27853  cusgrfilem1  29282  clwlknf1oclwwlknlem3  29906  occon  31110  spanss  31171  rmfsupp2  32959  fldgenss  33016  locfinreflem  33441  omsmon  33918  orvclteinc  34095  fin2solem  37079  poimirlem26  37119  poimirlem27  37120  cnambfre  37141  pclssN  39367  2polssN  39388  dihglblem3N  40768  dochss  40838  mapdordlem2  41110  nna4b4nsq  42084  itgoss  42587  nzss  43754  ovnsslelem  45948  rmsuppss  47434  mndpsuppss  47435  scmsuppss  47436