Theorem ss2rabdv 4054

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3140  {crab 3144   ⊆ wss 3938

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rab 3149  df-in 3945  df-ss 3954

This theorem is referenced by:  rabssrabd  4060  sess1  5525  suppssov1  7864  suppssfv  7868  harword  9031  mrcss  16889  ablfac1b  19194  mptscmfsupp0  19701  lspss  19758  aspss  20108  dsmmacl  20887  dsmmsubg  20889  dsmmlss  20890  scmatdmat  21126  clsss  21664  lfinpfin  22134  qustgpopn  22730  metss2lem  23123  equivcau  23905  rrxmvallem  24009  ovolsslem  24087  itg2monolem1  24353  lgamucov  25617  sqff1o  25761  musum  25770  cusgrfilem1  27239  clwlknf1oclwwlknlem3  27864  rmfsupp2  30868  locfinreflem  31106  omsmon  31558  orvclteinc  31735  fin2solem  34880  poimirlem26  34920  poimirlem27  34921  cnambfre  34942  pclssN  37032  2polssN  37053  dihglblem3N  38433  dochss  38503  mapdordlem2  38775  nzss  40656  rmsuppss  44425  mndpsuppss  44426  scmsuppss  44427