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

Theorem axc11r 2371
Description: Same as axc11 2435 but with reversed antecedent. Note the use of ax-12 2177 (and not merely ax12v 2178 as in axc11rv 2265).

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2053 and aecom 2432, 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 2377 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 2177 . . 3 (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
21sps 2185 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
3 pm2.27 42 . . 3 (𝑦 = 𝑥 → ((𝑦 = 𝑥𝜑) → 𝜑))
43al2imi 1815 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥𝜑) → ∀𝑦𝜑))
52, 4syld 47 1 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  ax12  2428  axc11n  2431  axc11  2435  hbae  2436  dral1  2444  dral1ALT  2445  sb4a  2485  axpowndlem3  10639  axc11n11r  36684  bj-ax12v3ALT  36687  bj-hbaeb2  36819
  Copyright terms: Public domain W3C validator