Theorem ralcom4 3262

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 1940	. . . 4 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑))
2	1	albii 1820	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
3		alcom 2164	. . 3 ⊢ (∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3052	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
5	2, 3, 4	3bitr4ri 304	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3052	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7	6	albii 1820	. 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	5, 7	bitr4i 278	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2162

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

This theorem is referenced by:  ralxpxfr2d  3600  uniiunlem  4039  iunssf  4998  iunssfOLD  4999  iunss  5000  iunssOLD  5001  disjor  5080  idrefALT  6070  funimass4  6898  fnssintima  7308  ralrnmpo  7497  imaeqalov  7597  ralxp3f  8079  findcard3  9183  ttrclss  9629  kmlem12  10072  fimaxre3  12088  vdwmc2  16907  ramtlecl  16928  iunocv  21636  1stccn  23407  itg2leub  25691  eqcuts2  27782  addsuniflem  27997  mulsuniflem  28145  mpteleeOLD  28968  nmoubi  30847  nmopub  31983  nmfnleub  32000  disjorf  32654  funcnv5mpt  32746  untuni  35903  elintfv  35959  heibor1lem  38010  ineleq  38547  inecmo  38548  pmapglbx  40029  ismnuprim  44535  setrec1lem2  49933