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	$$⊢\forall x\forall y\phi \to \forall y\forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		2stdpc4	$$⊢\forall x\forall y\phi \to \left[z/x\right]\left[t/y\right]\phi$$
2	1	gen2	$$⊢\forall t\forall z\left(\forall x\forall y\phi \to \left[z/x\right]\left[t/y\right]\phi \right)$$
3		nfv	$$⊢Ⅎt\phi$$
4	3	nfal	$$⊢Ⅎt\forall y\phi$$
5	4	nfal	$$⊢Ⅎt\forall x\forall y\phi$$
6		nfv	$$⊢Ⅎz\phi$$
7	6	nfal	$$⊢Ⅎz\forall y\phi$$
8	7	nfal	$$⊢Ⅎz\forall x\forall y\phi$$
9	5 8	2stdpc5	$$⊢\forall t\forall z\left(\forall x\forall y\phi \to \left[z/x\right]\left[t/y\right]\phi \right)\to \left(\forall x\forall y\phi \to \forall t\forall z\left[z/x\right]\left[t/y\right]\phi \right)$$
10	2 9	ax-mp	$$⊢\forall x\forall y\phi \to \forall t\forall z\left[z/x\right]\left[t/y\right]\phi$$
11	6	nfsbv	$$⊢Ⅎz\left[t/y\right]\phi$$
12	11	sb8f	$$⊢\forall x\left[t/y\right]\phi \leftrightarrow \forall z\left[z/x\right]\left[t/y\right]\phi$$
13	12	albii	$$⊢\forall t\forall x\left[t/y\right]\phi \leftrightarrow \forall t\forall z\left[z/x\right]\left[t/y\right]\phi$$
14	10 13	sylibr	$$⊢\forall x\forall y\phi \to \forall t\forall x\left[t/y\right]\phi$$
15		sbal	$$⊢\left[t/y\right]\forall x\phi \leftrightarrow \forall x\left[t/y\right]\phi$$
16	15	albii	$$⊢\forall t\left[t/y\right]\forall x\phi \leftrightarrow \forall t\forall x\left[t/y\right]\phi$$
17	14 16	sylibr	$$⊢\forall x\forall y\phi \to \forall t\left[t/y\right]\forall x\phi$$
18	3	nfal	$$⊢Ⅎt\forall x\phi$$
19	18	sb8f	$$⊢\forall y\forall x\phi \leftrightarrow \forall t\left[t/y\right]\forall x\phi$$
20	17 19	sylibr	$$⊢\forall x\forall y\phi \to \forall y\forall x\phi$$