Theorem axc11r 2399

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

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2088 and aecom 2458, 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 2403 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 2215	. . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
2	1	sps 2223	. 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 2215

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

This theorem is used by:  ax12  2454  axc11n  2457  axc11  2461  hbae  2462  dral1  2470  dral1ALT  2471  sb4a  2511  axpowndlem3  10612  axpowg2  35681  axpowg3  35682  axc11n11r  37424  bj-ax12v3ALT  37427  bj-hbaeb2  37569