Theorem eqoprab2b

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

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

Proof

Step	Hyp	Ref	Expression
1		ssoprab2b	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) )
2		ssoprab2b	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) )
3	1 2	anbi12i	⊢ ( ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ∧ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
4		eqss	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ∧ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ) )
5		2albiim	⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
6	5	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ↔ ∀ 𝑥 ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
7		19.26	⊢ ( ∀ 𝑥 ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
8	6 7	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜓 → 𝜑 ) ) )
9	3 4 8	3bitr4i	⊢ ( { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 ↔ 𝜓 ) )