Theorem axc11r 2372

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

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2057 and aecom 2431, 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 2376 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 2185	. . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
2	1	sps 2193	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
3		pm2.27 42	. . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑))
4	3	al2imi 1817	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑦𝜑))
5	2, 4	syld 47	1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  ax12  2427  axc11n  2430  axc11  2434  hbae  2435  dral1  2443  dral1ALT  2444  sb4a  2484  axpowndlem3  10522  axc11n11r  36980  bj-ax12v3ALT  36983  bj-hbaeb2  37125