Theorem ssopab2dv 5493

Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)

Hypothesis

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

Assertion

Ref	Expression
ssopab2dv	⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

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

Proof of Theorem ssopab2dv

Step	Hyp	Ref	Expression
1		ssopab2dv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	alrimivv 1935	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(𝜓 → 𝜒))
3		ssopab2 5488	. 2 ⊢ (∀𝑥∀𝑦(𝜓 → 𝜒) → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Syntax hints:   → wi 4  ∀wal 1545   ⊆ wss 3883  {copab 5134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-ss 3900  df-opab 5135

This theorem is referenced by:  xpss12  5633  coss1  5797  coss2  5798  cnvss  5814  aceq3lem  10033  coss12d  14925  shftfval  15023  sslm  23282  ulmval  26363  mptssALT  32766  fpwrelmap  32825  cossss  38882  dicssdvh  41678  rfovcnvf1od  44448