Theorem axc11r 2376

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

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

Syntax hints:   → wi 4  ∀wal 1545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  ax12  2431  axc11n  2434  axc11  2438  hbae  2439  dral1  2447  dral1ALT  2448  sb4a  2488  axpowndlem3  10520  axpowg2  35335  axpowg3  35336  axc11n11r  37033  bj-ax12v3ALT  37036  bj-hbaeb2  37178