Theorem ss2abdv 3965

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)

Hypothesis

Ref	Expression
ss2abdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ss2abdv	⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem ss2abdv

Step	Hyp	Ref	Expression
1		ss2abdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	alrimiv 1905	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))
3		ss2ab 3960	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ∀𝑥(𝜓 → 𝜒))
4	2, 3	sylibr 235	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4  ∀wal 1520  {cab 2775   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-in 3866  df-ss 3874

This theorem is referenced by:  intss  4803  ssopab2  5323  ssoprab2  7081  suppimacnvss  7691  suppimacnv  7692  ressuppss  7700  ss2ixp  8323  fiss  8734  tcss  9032  tcel  9033  infmap2  9486  cfub  9517  cflm  9518  cflecard  9521  clsslem  14178  cncmet  23608  plyss  24472  iunrnmptss  30007  ofrn2  30077  sigaclci  31008  subfacp1lem6  32040  ss2mcls  32423  itg2addnclem  34474  sdclem1  34550  istotbnd3  34581  sstotbnd  34585  qsss1  35077  aomclem4  39142  hbtlem4  39211  hbtlem3  39212  rngunsnply  39258  iocinico  39303