Description: Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable constraint. (Contributed by Wolf Lammen, 26-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-equsb4 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfeqf | ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 = 𝑧 ) | |
2 | 1 | ex | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑦 = 𝑧 ) ) |
3 | sbft | ⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) | |
4 | 2 3 | syl6com | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) ) |
5 | sbequ12r | ⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) | |
6 | 5 | equcoms | ⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) |
7 | 6 | sps | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) |
8 | 4 7 | pm2.61d2 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑦 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 ) ) |