Theorem ralcom 3264

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2162

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052

This theorem is referenced by:  rexcom  3265  ralrot3  3267  ralcom13  3268  2reu4lem  4476  ssint  4919  iinrab2  5025  disjxun  5096  reusv3  5350  cnvpo  6245  cnvso  6246  dfpo2  6254  fununi  6567  isocnv2  7277  dfsmo2  8279  tz7.48lem  8372  ixpiin  8862  boxriin  8878  dedekind  11296  rexfiuz  15271  gcdcllem1  16426  mreacs  17581  comfeq  17629  catpropd  17632  isnsg2  19085  cntzrec  19265  oppgsubm  19291  opprirred  20358  opprsubrng  20492  opprsubrg  20526  opprdomnb  20650  rmodislmodlem  20880  rmodislmod  20881  islindf4  21793  cpmatmcllem  22662  tgss2  22931  ist1-2  23291  kgencn  23500  ptcnplem  23565  cnmptcom  23622  fbun  23784  cnflf  23946  fclsopn  23958  cnfcf  23986  isclmp  25053  isncvsngp  25105  caucfil  25239  ovolgelb  25437  dyadmax  25555  ftc1a  26000  ulmcau  26360  noetasuplem4  27704  conway  27775  cofcutr  27920  addsprop  27972  onsfi  28352  perpcom  28785  colinearalg  28983  uhgrvd00  29608  pthdlem2lem  29840  frgrwopregbsn  30392  phoeqi  30932  ho02i  31904  hoeq2  31906  adjsym  31908  cnvadj  31967  mddmd2  32384  cdj3lem3b  32515  mgccnv  33081  cvmlift2lem12  35508  elpotr  35973  fvineqsnf1  37615  poimirlem29  37850  heicant  37856  ispsubsp2  40016  fsuppind  42843  nla0003  43676  ntrclsiso  44318  ntrneiiso  44342  ntrneik2  44343  ntrneix2  44344  ntrneik3  44347  ntrneix3  44348  ntrneik13  44349  ntrneix13  44350  ntrneik4w  44351  imo72b2  44423  tratrb  44787  hbra2VD  45110  tratrbVD  45111  termopropd  49499