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

Theorem axc11r 2366
Description: Same as axc11 2430 but with reversed antecedent. Note the use of ax-12 2172 (and not merely ax12v 2173 as in axc11rv 2258).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2057 and aecom 2427, 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 2372 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 2172 . . 3 (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
21sps 2179 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
3 pm2.27 42 . . 3 (𝑦 = 𝑥 → ((𝑦 = 𝑥𝜑) → 𝜑))
43al2imi 1818 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥𝜑) → ∀𝑦𝜑))
52, 4syld 47 1 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Colors of variables: wff setvar class
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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  ax12  2423  axc11n  2426  axc11  2430  hbae  2431  dral1  2439  dral1ALT  2440  sb4a  2484  axpowndlem3  10469  axc11n11r  35034  bj-ax12v3ALT  35037  bj-hbaeb2  35169
  Copyright terms: Public domain W3C validator