Theorem ralcom 3287

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-11 2155

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063

This theorem is referenced by:  rexcom  3288  ralrot3  3291  ralcom13  3292  ralcom13OLD  3293  2reu4lem  4526  ssint  4969  iinrab2  5074  disjxun  5147  reusv3  5404  cnvpo  6287  cnvso  6288  dfpo2  6296  fununi  6624  isocnv2  7328  dfsmo2  8347  tz7.48lem  8441  ixpiin  8918  boxriin  8934  dedekind  11377  rexfiuz  15294  gcdcllem1  16440  mreacs  17602  comfeq  17650  catpropd  17653  isnsg2  19036  cntzrec  19200  oppgsubm  19229  opprirred  20236  opprsubrg  20340  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  islindf4  21393  cpmatmcllem  22220  tgss2  22490  ist1-2  22851  kgencn  23060  ptcnplem  23125  cnmptcom  23182  fbun  23344  cnflf  23506  fclsopn  23518  cnfcf  23546  isclmp  24613  isncvsngp  24666  caucfil  24800  ovolgelb  24997  dyadmax  25115  ftc1a  25554  ulmcau  25907  noetasuplem4  27239  conway  27301  cofcutr  27413  addsprop  27462  perpcom  27995  colinearalg  28199  uhgrvd00  28822  pthdlem2lem  29055  frgrwopregbsn  29601  phoeqi  30141  ho02i  31113  hoeq2  31115  adjsym  31117  cnvadj  31176  mddmd2  31593  cdj3lem3b  31724  mgccnv  32200  cvmlift2lem12  34336  elpotr  34784  fvineqsnf1  36339  poimirlem29  36565  heicant  36571  ispsubsp2  38665  fsuppind  41210  nla0003  42224  ntrclsiso  42866  ntrneiiso  42890  ntrneik2  42891  ntrneix2  42892  ntrneik3  42895  ntrneix3  42896  ntrneik13  42897  ntrneix13  42898  ntrneik4w  42899  imo72b2  42972  tratrb  43345  hbra2VD  43669  tratrbVD  43670  opprsubrng  46786