Theorem ax11-pm2

Description: Proof of ax-11 from the standard axioms of predicate calculus, similar to PM's proof of alcom (PM*11.2). This proof requires that x and y be distinct. Axiom ax-11 is used in the proof only through nfal , nfsb , sbal , sb8 . See also ax11-pm . (Contributed by BJ, 15-Sep-2018) (Proof modification is discouraged.)

	Ref	Expression
Assertion	ax11-pm2	|- ( A. x A. y ph -> A. y A. x ph )

Proof

Step	Hyp	Ref	Expression
1		2stdpc4	|- ( A. x A. y ph -> [ z / x ] [ t / y ] ph )
2	1	gen2	|- A. t A. z ( A. x A. y ph -> [ z / x ] [ t / y ] ph )
3		nfv	|- F/ t ph
4	3	nfal	|- F/ t A. y ph
5	4	nfal	|- F/ t A. x A. y ph
6		nfv	|- F/ z ph
7	6	nfal	|- F/ z A. y ph
8	7	nfal	|- F/ z A. x A. y ph
9	5 8	2stdpc5	|- ( A. t A. z ( A. x A. y ph -> [ z / x ] [ t / y ] ph ) -> ( A. x A. y ph -> A. t A. z [ z / x ] [ t / y ] ph ) )
10	2 9	ax-mp	|- ( A. x A. y ph -> A. t A. z [ z / x ] [ t / y ] ph )
11	6	nfsbv	|- F/ z [ t / y ] ph
12	11	sb8v	|- ( A. x [ t / y ] ph <-> A. z [ z / x ] [ t / y ] ph )
13	12	albii	|- ( A. t A. x [ t / y ] ph <-> A. t A. z [ z / x ] [ t / y ] ph )
14	10 13	sylibr	|- ( A. x A. y ph -> A. t A. x [ t / y ] ph )
15		sbal	|- ( [ t / y ] A. x ph <-> A. x [ t / y ] ph )
16	15	albii	|- ( A. t [ t / y ] A. x ph <-> A. t A. x [ t / y ] ph )
17	14 16	sylibr	|- ( A. x A. y ph -> A. t [ t / y ] A. x ph )
18	3	nfal	|- F/ t A. x ph
19	18	sb8v	|- ( A. y A. x ph <-> A. t [ t / y ] A. x ph )
20	17 19	sylibr	|- ( A. x A. y ph -> A. y A. x ph )