Theorem sbal2

Description: Move quantifier in and out of substitution. Usage of this theorem is discouraged because it depends on ax-13 . Check out sbal for a version replacing the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 2-Jan-2002) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022) (Proof shortened by Wolf Lammen, 23-Sep-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	sbal2	|- ( -. A. x x = y -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ12	|- ( y = z -> ( A. x ph <-> [ z / y ] A. x ph ) )
2	1	sps	|- ( A. y y = z -> ( A. x ph <-> [ z / y ] A. x ph ) )
3		sbequ12	|- ( y = z -> ( ph <-> [ z / y ] ph ) )
4	3	sps	|- ( A. y y = z -> ( ph <-> [ z / y ] ph ) )
5	4	dral2	|- ( A. y y = z -> ( A. x ph <-> A. x [ z / y ] ph ) )
6	2 5	bitr3d	|- ( A. y y = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
7	6	adantl	|- ( ( -. A. x x = y /\ A. y y = z ) -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
8		sb4b	|- ( -. A. y y = z -> ( [ z / y ] A. x ph <-> A. y ( y = z -> A. x ph ) ) )
9	8	adantl	|- ( ( -. A. x x = y /\ -. A. y y = z ) -> ( [ z / y ] A. x ph <-> A. y ( y = z -> A. x ph ) ) )
10		nfnae	|- F/ x -. A. y y = z
11		sb4b	|- ( -. A. y y = z -> ( [ z / y ] ph <-> A. y ( y = z -> ph ) ) )
12	10 11	albid	|- ( -. A. y y = z -> ( A. x [ z / y ] ph <-> A. x A. y ( y = z -> ph ) ) )
13		alcom	|- ( A. x A. y ( y = z -> ph ) <-> A. y A. x ( y = z -> ph ) )
14	12 13	bitrdi	|- ( -. A. y y = z -> ( A. x [ z / y ] ph <-> A. y A. x ( y = z -> ph ) ) )
15		nfnae	|- F/ y -. A. x x = y
16		nfeqf1	|- ( -. A. x x = y -> F/ x y = z )
17		19.21t	|- ( F/ x y = z -> ( A. x ( y = z -> ph ) <-> ( y = z -> A. x ph ) ) )
18	16 17	syl	|- ( -. A. x x = y -> ( A. x ( y = z -> ph ) <-> ( y = z -> A. x ph ) ) )
19	15 18	albid	|- ( -. A. x x = y -> ( A. y A. x ( y = z -> ph ) <-> A. y ( y = z -> A. x ph ) ) )
20	14 19	sylan9bbr	|- ( ( -. A. x x = y /\ -. A. y y = z ) -> ( A. x [ z / y ] ph <-> A. y ( y = z -> A. x ph ) ) )
21	9 20	bitr4d	|- ( ( -. A. x x = y /\ -. A. y y = z ) -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
22	7 21	pm2.61dan	|- ( -. A. x x = y -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )