Theorem bj-ssbeq

Description: Substitution in an equality, disjoint variables case. Uses only ax-1 through ax-6 . It might be shorter to prove the result about composition of two substitutions and prove bj-ssbeq first with a DV condition on x , t , and then in the general case. (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ssbeq	⊢ ( [ 𝑡 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		df-sb	⊢ ( [ 𝑡 / 𝑥 ] 𝑦 = 𝑧 ↔ ∀ 𝑢 ( 𝑢 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ) )
2		19.23v	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑥 𝑥 = 𝑢 → 𝑦 = 𝑧 ) )
3		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑢
4		pm2.27	⊢ ( ∃ 𝑥 𝑥 = 𝑢 → ( ( ∃ 𝑥 𝑥 = 𝑢 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) )
5	3 4	ax-mp	⊢ ( ( ∃ 𝑥 𝑥 = 𝑢 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
6		ax-1	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 𝑥 = 𝑢 → 𝑦 = 𝑧 ) )
7	5 6	impbii	⊢ ( ( ∃ 𝑥 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ↔ 𝑦 = 𝑧 )
8	2 7	bitri	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ↔ 𝑦 = 𝑧 )
9	8	imbi2i	⊢ ( ( 𝑢 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ) ↔ ( 𝑢 = 𝑡 → 𝑦 = 𝑧 ) )
10	9	albii	⊢ ( ∀ 𝑢 ( 𝑢 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ) ↔ ∀ 𝑢 ( 𝑢 = 𝑡 → 𝑦 = 𝑧 ) )
11		19.23v	⊢ ( ∀ 𝑢 ( 𝑢 = 𝑡 → 𝑦 = 𝑧 ) ↔ ( ∃ 𝑢 𝑢 = 𝑡 → 𝑦 = 𝑧 ) )
12		ax6ev	⊢ ∃ 𝑢 𝑢 = 𝑡
13		pm2.27	⊢ ( ∃ 𝑢 𝑢 = 𝑡 → ( ( ∃ 𝑢 𝑢 = 𝑡 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 ) )
14	12 13	ax-mp	⊢ ( ( ∃ 𝑢 𝑢 = 𝑡 → 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
15		ax-1	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑢 𝑢 = 𝑡 → 𝑦 = 𝑧 ) )
16	14 15	impbii	⊢ ( ( ∃ 𝑢 𝑢 = 𝑡 → 𝑦 = 𝑧 ) ↔ 𝑦 = 𝑧 )
17	11 16	bitri	⊢ ( ∀ 𝑢 ( 𝑢 = 𝑡 → 𝑦 = 𝑧 ) ↔ 𝑦 = 𝑧 )
18	10 17	bitri	⊢ ( ∀ 𝑢 ( 𝑢 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑢 → 𝑦 = 𝑧 ) ) ↔ 𝑦 = 𝑧 )
19	1 18	bitri	⊢ ( [ 𝑡 / 𝑥 ] 𝑦 = 𝑧 ↔ 𝑦 = 𝑧 )