Theorem ralcom4 3177

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.)

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

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

Proof of Theorem ralcom4

Step	Hyp	Ref	Expression
1		19.21v 1899	. . . . 5 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑))
2	1	bicomi 216	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥 ∈ 𝐴 → 𝜑))
3	2	albii 1783	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑))
4		alcom 2096	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	3, 4	bitri 267	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑) ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3088	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
7		df-ral 3088	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	7	albii 1783	. 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
9	5, 6, 8	3bitr4i 295	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1506   ∈ wcel 2051  ∀wral 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-11 2094

This theorem depends on definitions:  df-bi 199  df-ex 1744  df-ral 3088

This theorem is referenced by:  ralxpxfr2d  3549  uniiunlem  3946  iunss  4832  disjor  4908  trintOLD  5044  reliun  5536  idrefALT  5811  funimass4  6558  ralrnmpo  7104  findcard3  8555  kmlem12  9380  fimaxre3  11387  vdwmc2  16170  ramtlecl  16191  iunocv  20543  1stccn  21791  itg2leub  24054  mptelee  26400  nmoubi  28342  nmopub  29482  nmfnleub  29499  moel  30050  disjorf  30113  funcnv5mpt  30193  untuni  32488  elintfv  32560  heibor1lem  34562  ineleq  35087  inecmo  35088  pmapglbx  36383  ss2iundf  39401  ismnuprim  40039  iunssf  40805  setrec1lem2  44188