Theorem ralcom4 3264

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

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

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 3053

This theorem is referenced by:  ralxpxfr2d  3602  uniiunlem  4041  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  disjor  5082  idrefALT  6078  funimass4  6906  fnssintima  7318  ralrnmpo  7507  imaeqalov  7607  ralxp3f  8089  findcard3  9195  ttrclss  9641  kmlem12  10084  fimaxre3  12100  vdwmc2  16919  ramtlecl  16940  iunocv  21648  1stccn  23419  itg2leub  25703  eqcuts2  27794  addsuniflem  28009  mulsuniflem  28157  mpteleeOLD  28980  nmoubi  30859  nmopub  31995  nmfnleub  32012  disjorf  32665  funcnv5mpt  32756  untuni  35922  elintfv  35978  heibor1lem  38057  ineleq  38602  inecmo  38603  pmapglbx  40142  ismnuprim  44647  setrec1lem2  50044