Theorem wl-sbcom2d

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

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

Proof

Step	Hyp	Ref	Expression
1		wl-sbcom2d.1	⊢ ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑤 )
2		wl-sbcom2d.2	⊢ ( 𝜑 → ¬ ∀ 𝑥 𝑥 = 𝑧 )
3		wl-sbcom2d.3	⊢ ( 𝜑 → ¬ ∀ 𝑧 𝑧 = 𝑦 )
4		ax6ev	⊢ ∃ 𝑢 𝑢 = 𝑦
5		ax6ev	⊢ ∃ 𝑣 𝑣 = 𝑤
6		wl-sbcom2d-lem2	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ) )
7		alcom	⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) )
8		ancomst	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) )
9	8	2albii	⊢ ( ∀ 𝑧 ∀ 𝑥 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) )
10	7 9	bitri	⊢ ( ∀ 𝑥 ∀ 𝑧 ( ( 𝑥 = 𝑢 ∧ 𝑧 = 𝑣 ) → 𝜓 ) ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) )
11	6 10	bitrdi	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) )
12	11	naecoms	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) )
13		wl-sbcom2d-lem2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ ∀ 𝑧 ∀ 𝑥 ( ( 𝑧 = 𝑣 ∧ 𝑥 = 𝑢 ) → 𝜓 ) ) )
14	12 13	bitr4d	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ) )
15	2 14	syl	⊢ ( 𝜑 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ) )
16	15	adantl	⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ) )
17		wl-sbcom2d-lem1	⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) )
18	1 17	syl5	⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( 𝜑 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) )
19	18	imp	⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) )
20		wl-sbcom2d-lem1	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑢 = 𝑦 ) → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) )
21	3 20	syl5	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑢 = 𝑦 ) → ( 𝜑 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) )
22	21	ancoms	⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( 𝜑 → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) ) )
23	22	imp	⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑣 / 𝑧 ] [ 𝑢 / 𝑥 ] 𝜓 ↔ [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ) )
24	16 19 23	3bitr3rd	⊢ ( ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) ∧ 𝜑 ) → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) )
25	24	exp31	⊢ ( 𝑢 = 𝑦 → ( 𝑣 = 𝑤 → ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) )
26	25	exlimdv	⊢ ( 𝑢 = 𝑦 → ( ∃ 𝑣 𝑣 = 𝑤 → ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) )
27	26	exlimiv	⊢ ( ∃ 𝑢 𝑢 = 𝑦 → ( ∃ 𝑣 𝑣 = 𝑤 → ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) ) ) )
28	4 5 27	mp2	⊢ ( 𝜑 → ( [ 𝑤 / 𝑧 ] [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜓 ) )