Metamath Proof Explorer


Theorem eqopab2b

Description: Equivalence of ordered pair abstraction equality and biconditional. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker eqopab2bw when possible. (Contributed by Mario Carneiro, 4-Jan-2017) (New usage is discouraged.)

Ref Expression
Assertion eqopab2b ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥𝑦 ( 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 ssopab2b ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥𝑦 ( 𝜑𝜓 ) )
2 ssopab2b ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥𝑦 ( 𝜓𝜑 ) )
3 1 2 anbi12i ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ( ∀ 𝑥𝑦 ( 𝜑𝜓 ) ∧ ∀ 𝑥𝑦 ( 𝜓𝜑 ) ) )
4 eqss ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
5 2albiim ( ∀ 𝑥𝑦 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥𝑦 ( 𝜑𝜓 ) ∧ ∀ 𝑥𝑦 ( 𝜓𝜑 ) ) )
6 3 4 5 3bitr4i ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥𝑦 ( 𝜑𝜓 ) )