Theorem ss2rabdv 4056

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∀wral 3050  {crab 3419   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rab 3420  df-ss 3948

This theorem is referenced by:  rabssrabd  4063  sess1  5630  suppssov1  8204  suppssov2  8205  suppssfv  8209  cofon1  8692  naddssim  8705  harword  9585  scottex  9907  mrcss  17630  mndpsuppss  18747  ablfac1b  20058  mptscmfsupp0  20893  lspss  20950  dsmmacl  21715  dsmmsubg  21717  dsmmlss  21718  aspss  21851  psdmul  22118  scmatdmat  22469  clsss  23008  lfinpfin  23478  qustgpopn  24074  metss2lem  24468  equivcau  25270  rrxmvallem  25374  ovolsslem  25455  itg2monolem1  25721  lgamucov  27017  sqff1o  27161  musum  27170  madess  27851  cofcut1  27890  cusgrfilem1  29401  clwlknf1oclwwlknlem3  30030  occon  31234  spanss  31295  rmfsupp2  33181  fldgenss  33258  locfinreflem  33798  omsmon  34259  orvclteinc  34437  fin2solem  37572  poimirlem26  37612  poimirlem27  37613  cnambfre  37634  pclssN  39855  2polssN  39876  dihglblem3N  41256  dochss  41326  mapdordlem2  41598  nna4b4nsq  42633  itgoss  43138  nzss  44293  ovnsslelem  46532  gpgusgralem  47969  rmsuppss  48244  scmsuppss  48245