Theorem axc11r 2372

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

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2056 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 2184	. . 3 ⊢ (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
2	1	sps 2192	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥 → 𝜑)))
3		pm2.27 42	. . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑥 → 𝜑) → 𝜑))
4	3	al2imi 1816	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥 → 𝜑) → ∀𝑦𝜑))
5	2, 4	syld 47	1 ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))

Syntax hints:   → wi 4  ∀wal 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

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

This theorem is referenced by:  ax12  2427  axc11n  2430  axc11  2434  hbae  2435  dral1  2443  dral1ALT  2444  sb4a  2484  axpowndlem3  10510  axc11n11r  36884  bj-ax12v3ALT  36887  bj-hbaeb2  37019