Theorem axc11r 2403

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

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2088 and aecom 2462, 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 2407 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.)

Assertion

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

Proof of Theorem axc11r

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  ax12  2458  axc11n  2461  axc11  2465  hbae  2466  dral1  2474  dral1ALT  2475  sb4a  2515  axpowndlem3  10602  axpowg2  35584  axpowg3  35585  axc11n11r  37349  bj-ax12v3ALT  37352  bj-hbaeb2  37494