Theorem ssopab2dv

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

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

Proof

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