Theorem ralcom2

Description: Commutation of restricted universal quantifiers. Note that x and y need not be disjoint (this makes the proof longer). If x and y are disjoint, then one may use ralcom . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ralcom2w when possible. (Contributed by NM, 24-Nov-1994) (Proof shortened by Mario Carneiro, 17-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Assertion	ralcom2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
2	1	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
3	2	imbi1d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜑 ) ) )
4	3	dral1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) ) )
5	4	bicomd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
6		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜑 ) )
7		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
8	5 6 7	3bitr4g	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 𝜑 ) )
9	2 8	imbi12d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
10	9	dral1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
11		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐴 𝜑 ) )
12		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
13	10 11 12	3bitr4g	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ) )
14	13	biimpd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ) )
15		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
16		nfra2	⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑
17	15 16	nfan	⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 )
18		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
19		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑
20	18 19	nfan	⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 )
21		nfcvf	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
22	21	adantr	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) → Ⅎ 𝑥 𝑦 )
23		nfcvd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) → Ⅎ 𝑥 𝐴 )
24	22 23	nfeld	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
25	20 24	nfan1	⊢ Ⅎ 𝑥 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) ∧ 𝑦 ∈ 𝐴 )
26		rsp2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝜑 ) )
27	26	ancomsd	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 ) )
28	27	expdimp	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
29	28	adantll	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
30	25 29	ralrimi	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝜑 )
31	30	ex	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) → ( 𝑦 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
32	17 31	ralrimi	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 )
33	32	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 ) )
34	14 33	pm2.61i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 𝜑 )