Theorem ss2rabdv 3824

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139  ∀wral 3050  {crab 3054   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-in 3722  df-ss 3729

This theorem is referenced by:  rabssrabd  3830  sess1  5234  suppfnssOLD  7489  suppssov1  7496  suppssfv  7500  harword  8635  mrcss  16478  ablfac1b  18669  mptscmfsupp0  19130  lspss  19186  aspss  19534  dsmmacl  20287  dsmmsubg  20289  dsmmlss  20290  scmatdmat  20523  clsss  21060  lfinpfin  21529  qustgpopn  22124  metss2lem  22517  equivcau  23298  rrxmvallem  23387  ovolsslem  23452  itg2monolem1  23716  lgamucov  24963  sqff1o  25107  musum  25116  cusgrfilem1  26561  clwlknf1oclwwlknlem3  27227  clwwlknonclwlknonf1olem  27521  locfinreflem  30216  omsmon  30669  orvclteinc  30846  fin2solem  33708  poimirlem26  33748  poimirlem27  33749  cnambfre  33771  pclssN  35683  2polssN  35704  dihglblem3N  37086  dochss  37156  mapdordlem2  37428  nzss  39018  rmsuppss  42661  mndpsuppss  42662  scmsuppss  42663