Theorem ralcom4 3287

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 1958	. . . 4 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → ∀𝑦𝜑))
2	1	albii 1838	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
3		alcom 2192	. . 3 ⊢ (∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → 𝜑))
4		df-ral 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦𝜑))
5	2, 3, 4	3bitr4ri 306	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3076	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7	6	albii 1838	. 2 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8	5, 7	bitr4i 280	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦𝜑 ↔ ∀𝑦∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-11 2190

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-ral 3076

This theorem is referenced by:  ralxpxfr2d  3604  uniiunlem  4038  iunssf  4997  iunssfOLD  4998  iunss  4999  iunssOLD  5000  disjor  5079  replem  5235  idrefALT  6096  funimass4  6926  fnssintima  7341  ralrnmpo  7530  imaeqalov  7630  ralxp3f  8111  findcard3  9221  ttrclss  9669  kmlem12  10112  fimaxre3  12132  vdwmc2  17006  ramtlecl  17027  iunocv  21721  1stccn  23511  itg2leub  25784  eqcuts2  27867  addsuniflem  28082  mulsuniflem  28230  mpteleeOLD  29053  nmoubi  30932  nmopub  32068  nmfnleub  32085  disjorf  32739  funcnv5mpt  32830  untuni  36020  elintfv  36076  heibor1lem  38269  ineleq  38814  inecmo  38815  pmapglbx  40354  ismnuprim  44831  setrec1lem2  50270