Metamath Proof Explorer


Theorem sbal2

Description: Move quantifier in and out of substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out sbal for a version replacing the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof shortened by Wolf Lammen, 23-Sep-2023) (New usage is discouraged.)

Ref Expression
Assertion sbal2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbequ12 ( 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) )
2 1 sps ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) )
3 sbequ12 ( 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
4 3 sps ( ∀ 𝑦 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
5 4 dral2 ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
6 2 5 bitr3d ( ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
7 6 adantl ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
8 sb4b ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
9 8 adantl ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
10 nfnae 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
11 sb4b ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧𝜑 ) ) )
12 10 11 albid ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥𝑦 ( 𝑦 = 𝑧𝜑 ) ) )
13 alcom ( ∀ 𝑥𝑦 ( 𝑦 = 𝑧𝜑 ) ↔ ∀ 𝑦𝑥 ( 𝑦 = 𝑧𝜑 ) )
14 12 13 bitrdi ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦𝑥 ( 𝑦 = 𝑧𝜑 ) ) )
15 nfnae 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
16 nfeqf1 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 = 𝑧 )
17 19.21t ( Ⅎ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑦 = 𝑧𝜑 ) ↔ ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
18 16 17 syl ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑦 = 𝑧𝜑 ) ↔ ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
19 15 18 albid ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦𝑥 ( 𝑦 = 𝑧𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
20 14 19 sylan9bbr ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
21 9 20 bitr4d ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
22 7 21 pm2.61dan ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )