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

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

This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2058 and aecom 2441, 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 2382 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 2176 . . 3 (𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
21sps 2183 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦(𝑦 = 𝑥𝜑)))
3 pm2.27 42 . . 3 (𝑦 = 𝑥 → ((𝑦 = 𝑥𝜑) → 𝜑))
43al2imi 1817 . 2 (∀𝑦 𝑦 = 𝑥 → (∀𝑦(𝑦 = 𝑥𝜑) → ∀𝑦𝜑))
52, 4syld 47 1 (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2176
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  ax12  2437  axc11n  2440  axc11  2444  hbae  2445  dral1  2453  dral1ALT  2454  sb4a  2501  axpowndlem3  10014  axc11n11r  34125  bj-ax12v3ALT  34128  bj-hbaeb2  34251
  Copyright terms: Public domain W3C validator