Metamath Proof Explorer


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 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥𝑦 ( 𝜑𝜓 ) )