Theorem eubiOLD

Description: Obsolete proof of eubi as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	eubiOLD	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝜑 ↔ 𝜓 )
2		sp	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( 𝜑 ↔ 𝜓 ) )
3	1 2	eubid	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 𝜓 ) )