Theorem ralcom 3287

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-11 2155

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060

This theorem is referenced by:  rexcom  3288  ralrot3  3291  ralcom13  3292  ralcom13OLD  3293  2reu4lem  4528  ssint  4969  iinrab2  5075  disjxun  5146  reusv3  5411  cnvpo  6309  cnvso  6310  dfpo2  6318  fununi  6643  isocnv2  7351  dfsmo2  8386  tz7.48lem  8480  ixpiin  8963  boxriin  8979  dedekind  11422  rexfiuz  15383  gcdcllem1  16533  mreacs  17703  comfeq  17751  catpropd  17754  isnsg2  19187  cntzrec  19367  oppgsubm  19396  opprirred  20439  opprsubrng  20576  opprsubrg  20610  opprdomnb  20734  rmodislmodlem  20944  rmodislmod  20945  rmodislmodOLD  20946  islindf4  21876  cpmatmcllem  22740  tgss2  23010  ist1-2  23371  kgencn  23580  ptcnplem  23645  cnmptcom  23702  fbun  23864  cnflf  24026  fclsopn  24038  cnfcf  24066  isclmp  25144  isncvsngp  25197  caucfil  25331  ovolgelb  25529  dyadmax  25647  ftc1a  26093  ulmcau  26453  noetasuplem4  27796  conway  27859  cofcutr  27973  addsprop  28024  perpcom  28736  colinearalg  28940  uhgrvd00  29567  pthdlem2lem  29800  frgrwopregbsn  30346  phoeqi  30886  ho02i  31858  hoeq2  31860  adjsym  31862  cnvadj  31921  mddmd2  32338  cdj3lem3b  32469  mgccnv  32974  cvmlift2lem12  35299  elpotr  35763  fvineqsnf1  37393  poimirlem29  37636  heicant  37642  ispsubsp2  39729  fsuppind  42577  nla0003  43415  ntrclsiso  44057  ntrneiiso  44081  ntrneik2  44082  ntrneix2  44083  ntrneik3  44086  ntrneix3  44087  ntrneik13  44088  ntrneix13  44089  ntrneik4w  44090  imo72b2  44162  tratrb  44534  hbra2VD  44858  tratrbVD  44859