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	$$⊢\left[t/x\right]y=z\leftrightarrow y=z$$

Proof

Step	Hyp	Ref	Expression
1		df-sb	$$⊢\left[t/x\right]y=z\leftrightarrow \forall u\left(u=t\to \forall x\left(x=u\to y=z\right)\right)$$
2		19.23v	$$⊢\forall x\left(x=u\to y=z\right)\leftrightarrow \left(\exists xx=u\to y=z\right)$$
3		ax6ev	$$⊢\exists xx=u$$
4		pm2.27	$$⊢\exists xx=u\to \left(\left(\exists xx=u\to y=z\right)\to y=z\right)$$
5	3 4	ax-mp	$$⊢\left(\exists xx=u\to y=z\right)\to y=z$$
6		ax-1	$$⊢y=z\to \left(\exists xx=u\to y=z\right)$$
7	5 6	impbii	$$⊢\left(\exists xx=u\to y=z\right)\leftrightarrow y=z$$
8	2 7	bitri	$$⊢\forall x\left(x=u\to y=z\right)\leftrightarrow y=z$$
9	8	imbi2i	$$⊢\left(u=t\to \forall x\left(x=u\to y=z\right)\right)\leftrightarrow \left(u=t\to y=z\right)$$
10	9	albii	$$⊢\forall u\left(u=t\to \forall x\left(x=u\to y=z\right)\right)\leftrightarrow \forall u\left(u=t\to y=z\right)$$
11		19.23v	$$⊢\forall u\left(u=t\to y=z\right)\leftrightarrow \left(\exists uu=t\to y=z\right)$$
12		ax6ev	$$⊢\exists uu=t$$
13		pm2.27	$$⊢\exists uu=t\to \left(\left(\exists uu=t\to y=z\right)\to y=z\right)$$
14	12 13	ax-mp	$$⊢\left(\exists uu=t\to y=z\right)\to y=z$$
15		ax-1	$$⊢y=z\to \left(\exists uu=t\to y=z\right)$$
16	14 15	impbii	$$⊢\left(\exists uu=t\to y=z\right)\leftrightarrow y=z$$
17	11 16	bitri	$$⊢\forall u\left(u=t\to y=z\right)\leftrightarrow y=z$$
18	10 17	bitri	$$⊢\forall u\left(u=t\to \forall x\left(x=u\to y=z\right)\right)\leftrightarrow y=z$$
19	1 18	bitri	$$⊢\left[t/x\right]y=z\leftrightarrow y=z$$