Metamath Proof Explorer


Theorem ax12fromc15

Description: Rederivation of Axiom ax-12 from ax-c15 , ax-c11 (used through dral1-o ), and other older axioms. See Theorem axc15 for the derivation of ax-c15 from ax-12 .

An open problem is whether we can prove this using ax-c11n instead of ax-c11 .

This proof uses newer axioms ax-4 and ax-6 , but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 and ax-c10 . (Contributed by NM, 22-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax12fromc15 ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 biidd ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑𝜑 ) )
2 1 dral1-o ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 𝜑 ) )
3 ax-1 ( 𝜑 → ( 𝑥 = 𝑦𝜑 ) )
4 3 alimi ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) )
5 2 4 syl6bir ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
6 5 a1d ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) ) )
7 ax-c5 ( ∀ 𝑦 𝜑𝜑 )
8 ax-c15 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) ) )
9 7 8 syl7 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) ) )
10 6 9 pm2.61i ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )