Theorem ss2rabdv 4055

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2113  ∀wral 3141  {crab 3145   ⊆ wss 3939

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rab 3150  df-in 3946  df-ss 3955

This theorem is referenced by:  rabssrabd  4061  sess1  5526  suppssov1  7865  suppssfv  7869  harword  9032  mrcss  16890  ablfac1b  19195  mptscmfsupp0  19702  lspss  19759  aspss  20109  dsmmacl  20888  dsmmsubg  20890  dsmmlss  20891  scmatdmat  21127  clsss  21665  lfinpfin  22135  qustgpopn  22731  metss2lem  23124  equivcau  23906  rrxmvallem  24010  ovolsslem  24088  itg2monolem1  24354  lgamucov  25618  sqff1o  25762  musum  25771  cusgrfilem1  27240  clwlknf1oclwwlknlem3  27865  rmfsupp2  30870  locfinreflem  31108  omsmon  31560  orvclteinc  31737  fin2solem  34882  poimirlem26  34922  poimirlem27  34923  cnambfre  34944  pclssN  37034  2polssN  37055  dihglblem3N  38435  dochss  38505  mapdordlem2  38777  nzss  40655  rmsuppss  44425  mndpsuppss  44426  scmsuppss  44427