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  27300  cofcutr  27411  addsprop  27460  perpcom  27964  colinearalg  28168  uhgrvd00  28791  pthdlem2lem  29024  frgrwopregbsn  29570  phoeqi  30110  ho02i  31082  hoeq2  31084  adjsym  31086  cnvadj  31145  mddmd2  31562  cdj3lem3b  31693  mgccnv  32169  cvmlift2lem12  34305  elpotr  34753  fvineqsnf1  36291  poimirlem29  36517  heicant  36523  ispsubsp2  38617  fsuppind  41162  nla0003  42176  ntrclsiso  42818  ntrneiiso  42842  ntrneik2  42843  ntrneix2  42844  ntrneik3  42847  ntrneix3  42848  ntrneik13  42849  ntrneix13  42850  ntrneik4w  42851  imo72b2  42924  tratrb  43297  hbra2VD  43621  tratrbVD  43622  opprsubrng  46738