Metamath Proof Explorer


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 ( ∀ 𝑥𝐴𝑦𝐴 𝜑 → ∀ 𝑦𝐴𝑥𝐴 𝜑 )

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 ( ∀ 𝑥𝐴𝑦𝐴 𝜑 → ∀ 𝑦𝐴𝑥𝐴 𝜑 )