Theorem ralcom 3257

Description: Commutation of restricted universal quantifiers. See ralcom2 3340 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3340 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 3165	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3165	. 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

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

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 3045

This theorem is referenced by:  rexcom  3258  ralrot3  3260  ralcom13  3261  2reu4lem  4473  ssint  4914  iinrab2  5019  disjxun  5090  reusv3  5344  cnvpo  6235  cnvso  6236  dfpo2  6244  fununi  6557  isocnv2  7268  dfsmo2  8270  tz7.48lem  8363  ixpiin  8851  boxriin  8867  dedekind  11279  rexfiuz  15255  gcdcllem1  16410  mreacs  17564  comfeq  17612  catpropd  17615  isnsg2  19035  cntzrec  19215  oppgsubm  19241  opprirred  20307  opprsubrng  20444  opprsubrg  20478  opprdomnb  20602  rmodislmodlem  20832  rmodislmod  20833  islindf4  21745  cpmatmcllem  22603  tgss2  22872  ist1-2  23232  kgencn  23441  ptcnplem  23506  cnmptcom  23563  fbun  23725  cnflf  23887  fclsopn  23899  cnfcf  23927  isclmp  24995  isncvsngp  25047  caucfil  25181  ovolgelb  25379  dyadmax  25497  ftc1a  25942  ulmcau  26302  noetasuplem4  27646  conway  27710  cofcutr  27837  addsprop  27888  onsfi  28252  perpcom  28658  colinearalg  28855  uhgrvd00  29480  pthdlem2lem  29712  frgrwopregbsn  30261  phoeqi  30801  ho02i  31773  hoeq2  31775  adjsym  31777  cnvadj  31836  mddmd2  32253  cdj3lem3b  32384  mgccnv  32941  cvmlift2lem12  35291  elpotr  35759  fvineqsnf1  37388  poimirlem29  37633  heicant  37639  ispsubsp2  39729  fsuppind  42567  nla0003  43402  ntrclsiso  44044  ntrneiiso  44068  ntrneik2  44069  ntrneix2  44070  ntrneik3  44073  ntrneix3  44074  ntrneik13  44075  ntrneix13  44076  ntrneik4w  44077  imo72b2  44149  tratrb  44514  hbra2VD  44837  tratrbVD  44838  termopropd  49233