MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axc11r Structured version   Visualization version   GIF version

Theorem axc11r 2368
Description: Same as axc11 2432 but with reversed antecedent. Note the use of ax-12 2174 (and not merely ax12v 2175 as in axc11rv 2262).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2050 and aecom 2429, 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 2374 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
StepHypRef Expression
1 ax-12 2174 . . 3 (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
21sps 2182 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
3 pm2.27 42 . . 3 (𝑦 = 𝑥 → ((𝑦 = 𝑥𝜑) → 𝜑))
43al2imi 1811 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥𝜑) → ∀𝑦𝜑))
52, 4syld 47 1 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174
This theorem depends on definitions:  df-bi 207  df-ex 1776
This theorem is referenced by:  ax12  2425  axc11n  2428  axc11  2432  hbae  2433  dral1  2441  dral1ALT  2442  sb4a  2482  axpowndlem3  10636  axc11n11r  36665  bj-ax12v3ALT  36668  bj-hbaeb2  36800
  Copyright terms: Public domain W3C validator