|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ax12w | Structured version Visualization version GIF version | ||
| Description: Weak version of ax-12 2176 from which we can prove any ax-12 2176 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. An instance of the first hypothesis will normally require that 𝑥 and 𝑦 be distinct (unless 𝑥 does not occur in 𝜑). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for 𝜑, see ax12wdemo 2134. (Contributed by NM, 10-Apr-2017.) | 
| Ref | Expression | 
|---|---|
| ax12w.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | 
| ax12w.2 | ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) | 
| Ref | Expression | 
|---|---|
| ax12w | ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ax12w.2 | . . 3 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒)) | |
| 2 | 1 | spw 2032 | . 2 ⊢ (∀𝑦𝜑 → 𝜑) | 
| 3 | ax12w.1 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | ax12wlem 2131 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | 
| 5 | 2, 4 | syl5 34 | 1 ⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1537 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: ax12wdemo 2134 | 
| Copyright terms: Public domain | W3C validator |