Theorem ss2rabdv 4026

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047  {crab 3395   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rab 3396  df-ss 3919

This theorem is referenced by:  rabssrabd  4033  sess1  5581  suppssov1  8127  suppssov2  8128  suppssfv  8132  cofon1  8587  naddssim  8600  harword  9449  scottex  9778  mrcss  17522  mndpsuppss  18673  ablfac1b  19985  mptscmfsupp0  20861  lspss  20918  dsmmacl  21679  dsmmsubg  21681  dsmmlss  21682  aspss  21815  psdmul  22082  scmatdmat  22431  clsss  22970  lfinpfin  23440  qustgpopn  24036  metss2lem  24427  equivcau  25228  rrxmvallem  25332  ovolsslem  25413  itg2monolem1  25679  lgamucov  26976  sqff1o  27120  musum  27129  madess  27822  cofcut1  27865  bdayon  28210  cusgrfilem1  29435  clwlknf1oclwwlknlem3  30061  occon  31265  spanss  31326  rmfsupp2  33203  fldgenss  33280  locfinreflem  33851  omsmon  34309  orvclteinc  34487  rankval4b  35109  fin2solem  37652  poimirlem26  37692  poimirlem27  37693  cnambfre  37714  pclssN  39939  2polssN  39960  dihglblem3N  41340  dochss  41410  mapdordlem2  41682  nna4b4nsq  42699  itgoss  43202  nzss  44356  ovnsslelem  46604  gpgusgralem  48093  rmsuppss  48407  scmsuppss  48408