Metamath Proof Explorer

Theorem wl-2sb6d

Description: Version of 2sb6 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019)

Ref Expression
Hypotheses wl-2sb6d.1 ⊢ ( 𝜑 → ¬ ∀ 𝑦 𝑦 = 𝑥 )
wl-2sb6d.2 ⊢ ( 𝜑 → ¬ ∀ 𝑦 𝑦 = 𝑤 )
wl-2sb6d.3 ⊢ ( 𝜑 → ¬ ∀ 𝑦 𝑦 = 𝑧 )
wl-2sb6d.4 ⊢ ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑧 )
Assertion wl-2sb6d ( 𝜑 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 wl-2sb6d.1 ⊢ ( 𝜑 → ¬ ∀ 𝑦 𝑦 = 𝑥 )
2 wl-2sb6d.2 ⊢ ( 𝜑 → ¬ ∀ 𝑦 𝑦 = 𝑤 )
3 wl-2sb6d.3 ⊢ ( 𝜑 → ¬ ∀ 𝑦 𝑦 = 𝑧 )
4 wl-2sb6d.4 ⊢ ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑧 )
5 1 3 jca ⊢ ( 𝜑 → ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) )
6 sb4b ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜓 ) ) )
7 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑤
8 wl-nfnae1 ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑥
9 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
10 8 9 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 )
11 7 10 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑦 𝑦 = 𝑤 ∧ ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) )
12 sb4b ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑤 → ( [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜓 ) ) )
13 12 imbi2d ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑤 → ( ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜓 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜓 ) ) ) )
14 impexp ⊢ ( ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ↔ ( 𝑥 = 𝑧 → ( 𝑦 = 𝑤 → 𝜓 ) ) )
15 14 albii ⊢ ( ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ↔ ∀ 𝑦 ( 𝑥 = 𝑧 → ( 𝑦 = 𝑤 → 𝜓 ) ) )
16 nfeqf ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → Ⅎ 𝑦 𝑥 = 𝑧 )
17 19.21t ⊢ ( Ⅎ 𝑦 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑥 = 𝑧 → ( 𝑦 = 𝑤 → 𝜓 ) ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜓 ) ) ) )
18 16 17 syl ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑦 ( 𝑥 = 𝑧 → ( 𝑦 = 𝑤 → 𝜓 ) ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜓 ) ) ) )
19 15 18 bitr2id ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ( 𝑥 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜓 ) ) ↔ ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ) )
20 13 19 sylan9bb ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑤 ∧ ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ) → ( ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ) )
21 11 20 albid ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑤 ∧ ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ) )
22 6 21 sylan9bb ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑦 𝑦 = 𝑤 ∧ ( ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) ) ) → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ) )
23 4 2 5 22 syl12anc ⊢ ( 𝜑 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜓 ) ) )