Theorem ralcom 3266

Description: Commutation of restricted universal quantifiers. See ralcom2 3353 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3353 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

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

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		ancomst 464	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
2	1	2albii 1820	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
3		alcom 2160	. . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
5		r2al 3174	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3174	. 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3046

This theorem is referenced by:  rexcom  3267  ralrot3  3270  ralcom13  3271  ralcom13OLD  3272  2reu4lem  4488  ssint  4931  iinrab2  5037  disjxun  5108  reusv3  5363  cnvpo  6263  cnvso  6264  dfpo2  6272  fununi  6594  isocnv2  7309  dfsmo2  8319  tz7.48lem  8412  ixpiin  8900  boxriin  8916  dedekind  11344  rexfiuz  15321  gcdcllem1  16476  mreacs  17626  comfeq  17674  catpropd  17677  isnsg2  19095  cntzrec  19275  oppgsubm  19301  opprirred  20338  opprsubrng  20475  opprsubrg  20509  opprdomnb  20633  rmodislmodlem  20842  rmodislmod  20843  islindf4  21754  cpmatmcllem  22612  tgss2  22881  ist1-2  23241  kgencn  23450  ptcnplem  23515  cnmptcom  23572  fbun  23734  cnflf  23896  fclsopn  23908  cnfcf  23936  isclmp  25004  isncvsngp  25056  caucfil  25190  ovolgelb  25388  dyadmax  25506  ftc1a  25951  ulmcau  26311  noetasuplem4  27655  conway  27718  cofcutr  27839  addsprop  27890  onsfi  28254  perpcom  28647  colinearalg  28844  uhgrvd00  29469  pthdlem2lem  29704  frgrwopregbsn  30253  phoeqi  30793  ho02i  31765  hoeq2  31767  adjsym  31769  cnvadj  31828  mddmd2  32245  cdj3lem3b  32376  mgccnv  32932  cvmlift2lem12  35308  elpotr  35776  fvineqsnf1  37405  poimirlem29  37650  heicant  37656  ispsubsp2  39747  fsuppind  42585  nla0003  43421  ntrclsiso  44063  ntrneiiso  44087  ntrneik2  44088  ntrneix2  44089  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  ntrneik4w  44096  imo72b2  44168  tratrb  44533  hbra2VD  44856  tratrbVD  44857  termopropd  49237