Theorem ss2abdv 4043

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

Syntax hints:   → wi 4  ∀wal 1531  {cab 2799   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951

This theorem is referenced by:  intss  4896  ssopab2  5432  ssoprab2  7221  suppimacnvss  7839  suppimacnv  7840  ressuppss  7848  ss2ixp  8473  fiss  8887  tcss  9185  tcel  9186  infmap2  9639  cfub  9670  cflm  9671  cflecard  9674  clsslem  14343  cncmet  23924  plyss  24788  iunrnmptss  30316  ofrn2  30386  sigaclci  31391  subfacp1lem6  32432  ss2mcls  32815  itg2addnclem  34942  sdclem1  35017  istotbnd3  35048  sstotbnd  35052  qsss1  35544  aomclem4  39655  hbtlem4  39724  hbtlem3  39725  rngunsnply  39771  iocinico  39816