Theorem axc11r

Description: Same as axc11 but with reversed antecedent. Note the use of ax-12 (and not merely ax12v as in axc11rv ).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev and aecom , for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015)

	Ref	Expression
Assertion	axc11r	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-12	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ) )
2	1	sps	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ) )
3		pm2.27	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 = 𝑥 → 𝜑 ) → 𝜑 ) )
4	3	al2imi	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) → ∀ 𝑦 𝜑 ) )
5	2 4	syld	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) )