equs5

Description: Lemma used in proofs of substitution properties. If there is a disjoint variable condition on x , y , then sbalex can be used instead; if y is not free in ph , then equs45f can be used. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 14-May-1993) (Revised by BJ, 1-Oct-2018) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfna1	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
2		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 )
3		axc15	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
4	3	impd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
5	1 2 4	exlimd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
6		equs4	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
7	5 6	impbid1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )

Metamath Proof Explorer

Theorem equs5

Proof