Theorem ssopab2i

Description: Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995)

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

Proof

Step	Hyp	Ref	Expression
1		ssopab2i.1	⊢ ( 𝜑 → 𝜓 )
2		ssopab2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
3	1	ax-gen	⊢ ∀ 𝑦 ( 𝜑 → 𝜓 )
4	2 3	mpg	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }