Theorem ralcom2

Description: Commutation of restricted universal quantifiers. Note that x and y need not be disjoint (this makes the proof longer). This theorem relies on the full set of axioms up to ax-ext and it should no longer be used. Usage of ralcom is highly encouraged. (Contributed by NM, 24-Nov-1994) (Proof shortened by Mario Carneiro, 17-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	ralcom2	$$⊢\forall x\in A\forall y\in A\phi \to \forall y\in A\forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
2	1	sps	$$⊢\forall xx=y\to \left(x\in A\leftrightarrow y\in A\right)$$
3	2	imbi1d	$$⊢\forall xx=y\to \left(\left(x\in A\to \phi \right)\leftrightarrow \left(y\in A\to \phi \right)\right)$$
4	3	dral1	$$⊢\forall xx=y\to \left(\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall y\left(y\in A\to \phi \right)\right)$$
5	4	bicomd	$$⊢\forall xx=y\to \left(\forall y\left(y\in A\to \phi \right)\leftrightarrow \forall x\left(x\in A\to \phi \right)\right)$$
6		df-ral	$$⊢\forall y\in A\phi \leftrightarrow \forall y\left(y\in A\to \phi \right)$$
7		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
8	5 6 7	3bitr4g	$$⊢\forall xx=y\to \left(\forall y\in A\phi \leftrightarrow \forall x\in A\phi \right)$$
9	2 8	imbi12d	$$⊢\forall xx=y\to \left(\left(x\in A\to \forall y\in A\phi \right)\leftrightarrow \left(y\in A\to \forall x\in A\phi \right)\right)$$
10	9	dral1	$$⊢\forall xx=y\to \left(\forall x\left(x\in A\to \forall y\in A\phi \right)\leftrightarrow \forall y\left(y\in A\to \forall x\in A\phi \right)\right)$$
11		df-ral	$$⊢\forall x\in A\forall y\in A\phi \leftrightarrow \forall x\left(x\in A\to \forall y\in A\phi \right)$$
12		df-ral	$$⊢\forall y\in A\forall x\in A\phi \leftrightarrow \forall y\left(y\in A\to \forall x\in A\phi \right)$$
13	10 11 12	3bitr4g	$$⊢\forall xx=y\to \left(\forall x\in A\forall y\in A\phi \leftrightarrow \forall y\in A\forall x\in A\phi \right)$$
14	13	biimpd	$$⊢\forall xx=y\to \left(\forall x\in A\forall y\in A\phi \to \forall y\in A\forall x\in A\phi \right)$$
15		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
16		nfra2	$$⊢Ⅎy\forall x\in A\forall y\in A\phi$$
17	15 16	nfan	$$⊢Ⅎy\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)$$
18		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
19		nfra1	$$⊢Ⅎx\forall x\in A\forall y\in A\phi$$
20	18 19	nfan	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)$$
21		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
22	21	adantr	$$⊢\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\to \underset{\_}{Ⅎ}xy$$
23		nfcvd	$$⊢\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\to \underset{\_}{Ⅎ}xA$$
24	22 23	nfeld	$$⊢\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\to Ⅎxy\in A$$
25	20 24	nfan1	$$⊢Ⅎx\left(\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\wedge y\in A\right)$$
26		rsp2	$$⊢\forall x\in A\forall y\in A\phi \to \left(\left(x\in A\wedge y\in A\right)\to \phi \right)$$
27	26	ancomsd	$$⊢\forall x\in A\forall y\in A\phi \to \left(\left(y\in A\wedge x\in A\right)\to \phi \right)$$
28	27	expdimp	$$⊢\left(\forall x\in A\forall y\in A\phi \wedge y\in A\right)\to \left(x\in A\to \phi \right)$$
29	28	adantll	$$⊢\left(\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\wedge y\in A\right)\to \left(x\in A\to \phi \right)$$
30	25 29	ralrimi	$$⊢\left(\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\wedge y\in A\right)\to \forall x\in A\phi$$
31	30	ex	$$⊢\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\to \left(y\in A\to \forall x\in A\phi \right)$$
32	17 31	ralrimi	$$⊢\left(\neg \forall xx=y\wedge \forall x\in A\forall y\in A\phi \right)\to \forall y\in A\forall x\in A\phi$$
33	32	ex	$$⊢\neg \forall xx=y\to \left(\forall x\in A\forall y\in A\phi \to \forall y\in A\forall x\in A\phi \right)$$
34	14 33	pm2.61i	$$⊢\forall x\in A\forall y\in A\phi \to \forall y\in A\forall x\in A\phi$$