Theorem ss2rabdv 3646

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  {crab 2900   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-in 3547  df-ss 3554

This theorem is referenced by:  sess1  5006  suppfnss  7207  suppssov1  7214  suppssfv  7218  harword  8353  mrcss  16099  ablfac1b  18292  mptscmfsupp0  18751  lspss  18805  aspss  19153  dsmmacl  19904  dsmmsubg  19906  dsmmlss  19907  scmatdmat  20140  clsss  20668  lfinpfin  21137  qustgpopn  21733  metss2lem  22126  equivcau  22906  rrxmvallem  22995  ovolsslem  23059  itg2monolem1  23323  lgamucov  24564  sqff1o  24708  musum  24717  cusgrafilem1  26007  locfinreflem  29235  omsmon  29687  orvclteinc  29864  fin2solem  32565  poimirlem26  32605  poimirlem27  32606  cnambfre  32628  pclssN  34198  2polssN  34219  dihglblem3N  35602  dochss  35672  mapdordlem2  35944  nzss  37538  cusgrfilem1  40671  rmsuppss  41945  mndpsuppss  41946  scmsuppss  41947