Theorem ss2abdv 3708

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 1895	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 → 𝜒))
3		ss2ab 3703	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒} ↔ ∀𝑥(𝜓 → 𝜒))
4	2, 3	sylibr 224	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4  ∀wal 1521  {cab 2637   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621

This theorem is referenced by:  intss  4530  ssopab2  5030  ssoprab2  6753  suppimacnvss  7350  suppimacnv  7351  ressuppss  7359  ss2ixp  7963  fiss  8371  tcss  8658  tcel  8659  infmap2  9078  cfub  9109  cflm  9110  cflecard  9113  clsslem  13769  cncmet  23165  plyss  24000  ofrn2  29570  sigaclci  30323  subfacp1lem6  31293  ss2mcls  31591  itg2addnclem  33591  sdclem1  33669  istotbnd3  33700  sstotbnd  33704  qsss1  34194  aomclem4  37944  hbtlem4  38013  hbtlem3  38014  rngunsnply  38060  iocinico  38114