Description: An alternate definition of proper substitution df-sb that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 6-Mar-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfsb3 | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-or | ⊢ ( ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ( ¬ ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) | |
| 2 | dfsb2 | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) | |
| 3 | imnan | ⊢ ( ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ( 𝑥 = 𝑦 ∧ 𝜑 ) ) | |
| 4 | 3 | imbi1i | ⊢ ( ( ( 𝑥 = 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ( ¬ ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |
| 5 | 1 2 4 | 3bitr4i | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) |