Theorem equs3OLD

Description: Obsolete as of 12-Aug-2023. Use alinexa or sbn instead. Lemma used in proofs of substitution properties. (Contributed by NM, 10-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	equs3OLD	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		alinexa	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
2	1	con2bii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) )