Theorem ss2abdv 3638

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

Syntax hints:   → wi 4  ∀wal 1473  {cab 2596   ⊆ 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-in 3547  df-ss 3554

This theorem is referenced by:  intss  4433  ssopab2  4926  ssoprab2  6609  suppimacnvss  7192  suppimacnv  7193  ressuppss  7201  ss2ixp  7807  fiss  8213  tcss  8503  tcel  8504  infmap2  8923  cfub  8954  cflm  8955  cflecard  8958  clsslem  13571  cncmet  22927  plyss  23759  ofrn2  28822  sigaclci  29522  subfacp1lem6  30421  ss2mcls  30719  itg2addnclem  32631  sdclem1  32709  istotbnd3  32740  sstotbnd  32744  aomclem4  36645  hbtlem4  36715  hbtlem3  36716  rngunsnply  36762  iocinico  36816