Theorem ralcom4 3263

Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)

Assertion

Ref	Expression
ralcom4	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem ralcom4

Step	Hyp	Ref	Expression
1		19.21v 1941	. . . 4 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑))
2	1	albii 1821	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
3		alcom 2165	. . 3 ⊢ (∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3052	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
5	2, 3, 4	3bitr4ri 304	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3052	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7	6	albii 1821	. 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	5, 7	bitr4i 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-ral 3052

This theorem is referenced by:  ralxpxfr2d  3588  uniiunlem  4027  iunssf  4985  iunssfOLD  4986  iunss  4987  iunssOLD  4988  disjor  5067  replem  5223  idrefALT  6076  funimass4  6904  fnssintima  7317  ralrnmpo  7506  imaeqalov  7606  ralxp3f  8087  findcard3  9193  ttrclss  9641  kmlem12  10084  fimaxre3  12102  vdwmc2  16950  ramtlecl  16971  iunocv  21661  1stccn  23428  itg2leub  25701  eqcuts2  27778  addsuniflem  27993  mulsuniflem  28141  mpteleeOLD  28964  nmoubi  30843  nmopub  31979  nmfnleub  31996  disjorf  32649  funcnv5mpt  32740  untuni  35891  elintfv  35947  heibor1lem  38130  ineleq  38675  inecmo  38676  pmapglbx  40215  ismnuprim  44721  setrec1lem2  50163