Theorem ss2rabdv 4074

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062  {crab 3433   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  rabssrabd  4082  sess1  5645  suppssov1  8183  suppssfv  8187  cofon1  8671  naddssim  8684  harword  9558  scottex  9880  mrcss  17560  ablfac1b  19940  mptscmfsupp0  20537  lspss  20595  dsmmacl  21296  dsmmsubg  21298  dsmmlss  21299  aspss  21431  scmatdmat  22017  clsss  22558  lfinpfin  23028  qustgpopn  23624  metss2lem  24020  equivcau  24817  rrxmvallem  24921  ovolsslem  25001  itg2monolem1  25268  lgamucov  26542  sqff1o  26686  musum  26695  madess  27371  cofcut1  27407  cusgrfilem1  28712  clwlknf1oclwwlknlem3  29336  occon  30540  spanss  30601  rmfsupp2  32387  fldgenss  32406  locfinreflem  32820  omsmon  33297  orvclteinc  33474  fin2solem  36474  poimirlem26  36514  poimirlem27  36515  cnambfre  36536  pclssN  38765  2polssN  38786  dihglblem3N  40166  dochss  40236  mapdordlem2  40508  nna4b4nsq  41402  itgoss  41905  nzss  43076  ovnsslelem  45276  rmsuppss  47046  mndpsuppss  47047  scmsuppss  47048