Theorem ssopab2b

Description: Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ssopab2bw when possible. (Contributed by NM, 27-Dec-1996) (Proof shortened by Mario Carneiro, 18-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	ssopab2b	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }
3	1 2	nfss	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }
4		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
5		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }
6	4 5	nfss	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }
7		ssel	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
8		opabid	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
9		opabid	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ 𝜓 )
10	7 8 9	3imtr3g	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → ( 𝜑 → 𝜓 ) )
11	6 10	alrimi	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → ∀ 𝑦 ( 𝜑 → 𝜓 ) )
12	3 11	alrimi	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )
13		ssopab2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
14	12 13	impbii	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )