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 | ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| 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 | ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |