This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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