Theorem ralcom 3295

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068

This theorem is referenced by:  rexcom  3296  ralrot3  3299  ralcom13  3300  ralcom13OLD  3301  2reu4lem  4545  ssint  4988  iinrab2  5093  disjxun  5164  reusv3  5423  cnvpo  6318  cnvso  6319  dfpo2  6327  fununi  6653  isocnv2  7367  dfsmo2  8403  tz7.48lem  8497  ixpiin  8982  boxriin  8998  dedekind  11453  rexfiuz  15396  gcdcllem1  16545  mreacs  17716  comfeq  17764  catpropd  17767  isnsg2  19196  cntzrec  19376  oppgsubm  19405  opprirred  20448  opprsubrng  20585  opprsubrg  20621  opprdomnb  20739  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  islindf4  21881  cpmatmcllem  22745  tgss2  23015  ist1-2  23376  kgencn  23585  ptcnplem  23650  cnmptcom  23707  fbun  23869  cnflf  24031  fclsopn  24043  cnfcf  24071  isclmp  25149  isncvsngp  25202  caucfil  25336  ovolgelb  25534  dyadmax  25652  ftc1a  26098  ulmcau  26456  noetasuplem4  27799  conway  27862  cofcutr  27976  addsprop  28027  perpcom  28739  colinearalg  28943  uhgrvd00  29570  pthdlem2lem  29803  frgrwopregbsn  30349  phoeqi  30889  ho02i  31861  hoeq2  31863  adjsym  31865  cnvadj  31924  mddmd2  32341  cdj3lem3b  32472  mgccnv  32972  cvmlift2lem12  35282  elpotr  35745  fvineqsnf1  37376  poimirlem29  37609  heicant  37615  ispsubsp2  39703  fsuppind  42545  nla0003  43387  ntrclsiso  44029  ntrneiiso  44053  ntrneik2  44054  ntrneix2  44055  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  ntrneik4w  44062  imo72b2  44134  tratrb  44507  hbra2VD  44831  tratrbVD  44832