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  4525  ssint  4968  iinrab2  5073  disjxun  5146  reusv3  5403  cnvpo  6284  cnvso  6285  dfpo2  6293  fununi  6621  isocnv2  7325  dfsmo2  8344  tz7.48lem  8438  ixpiin  8915  boxriin  8931  dedekind  11374  rexfiuz  15291  gcdcllem1  16437  mreacs  17599  comfeq  17647  catpropd  17650  isnsg2  19031  cntzrec  19195  oppgsubm  19224  opprirred  20229  opprsubrg  20377  rmodislmodlem  20532  rmodislmod  20533  rmodislmodOLD  20534  islindf4  21385  cpmatmcllem  22212  tgss2  22482  ist1-2  22843  kgencn  23052  ptcnplem  23117  cnmptcom  23174  fbun  23336  cnflf  23498  fclsopn  23510  cnfcf  23538  isclmp  24605  isncvsngp  24658  caucfil  24792  ovolgelb  24989  dyadmax  25107  ftc1a  25546  ulmcau  25899  noetasuplem4  27229  conway  27290  cofcutr  27401  addsprop  27450  perpcom  27954  colinearalg  28158  uhgrvd00  28781  pthdlem2lem  29014  frgrwopregbsn  29560  phoeqi  30098  ho02i  31070  hoeq2  31072  adjsym  31074  cnvadj  31133  mddmd2  31550  cdj3lem3b  31681  mgccnv  32157  cvmlift2lem12  34294  elpotr  34742  fvineqsnf1  36280  poimirlem29  36506  heicant  36512  ispsubsp2  38606  fsuppind  41160  nla0003  42162  ntrclsiso  42804  ntrneiiso  42828  ntrneik2  42829  ntrneix2  42830  ntrneik3  42833  ntrneix3  42834  ntrneik13  42835  ntrneix13  42836  ntrneik4w  42837  imo72b2  42910  tratrb  43283  hbra2VD  43607  tratrbVD  43608  opprsubrng  46723