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	|- ( [ t / x ] y = z <-> y = z )

Proof

Step	Hyp	Ref	Expression
1		df-sb	|- ( [ t / x ] y = z <-> A. u ( u = t -> A. x ( x = u -> y = z ) ) )
2		19.23v	|- ( A. x ( x = u -> y = z ) <-> ( E. x x = u -> y = z ) )
3		ax6ev	|- E. x x = u
4		pm2.27	|- ( E. x x = u -> ( ( E. x x = u -> y = z ) -> y = z ) )
5	3 4	ax-mp	|- ( ( E. x x = u -> y = z ) -> y = z )
6		ax-1	|- ( y = z -> ( E. x x = u -> y = z ) )
7	5 6	impbii	|- ( ( E. x x = u -> y = z ) <-> y = z )
8	2 7	bitri	|- ( A. x ( x = u -> y = z ) <-> y = z )
9	8	imbi2i	|- ( ( u = t -> A. x ( x = u -> y = z ) ) <-> ( u = t -> y = z ) )
10	9	albii	|- ( A. u ( u = t -> A. x ( x = u -> y = z ) ) <-> A. u ( u = t -> y = z ) )
11		19.23v	|- ( A. u ( u = t -> y = z ) <-> ( E. u u = t -> y = z ) )
12		ax6ev	|- E. u u = t
13		pm2.27	|- ( E. u u = t -> ( ( E. u u = t -> y = z ) -> y = z ) )
14	12 13	ax-mp	|- ( ( E. u u = t -> y = z ) -> y = z )
15		ax-1	|- ( y = z -> ( E. u u = t -> y = z ) )
16	14 15	impbii	|- ( ( E. u u = t -> y = z ) <-> y = z )
17	11 16	bitri	|- ( A. u ( u = t -> y = z ) <-> y = z )
18	10 17	bitri	|- ( A. u ( u = t -> A. x ( x = u -> y = z ) ) <-> y = z )
19	1 18	bitri	|- ( [ t / x ] y = z <-> y = z )