Theorem ralcom 3293

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-11 2192

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080

This theorem is referenced by:  rexcom  3294  ralrot3  3296  ralcom13  3297  2reu4lem  4484  ssint  4929  iinrab2  5034  disjxun  5107  reusv3  5376  cnvpo  6288  cnvso  6289  dfpo2  6297  fununi  6611  isocnv2  7329  dfsmo2  8330  tz7.48lem  8424  ixpiin  8918  boxriin  8934  dedekind  11368  rexfiuz  15395  gcdcllem1  16552  mreacs  17709  comfeq  17757  catpropd  17760  isnsg2  19217  cntzrec  19401  oppgsubm  19427  opprirred  20500  opprsubrng  20658  opprsubrg  20692  opprdomnb  20815  rmodislmodlem  21050  rmodislmod  21051  islindf4  21988  cpmatmcllem  22875  tgss2  23144  ist1-2  23504  kgencn  23713  ptcnplem  23778  cnmptcom  23835  fbun  23997  cnflf  24159  fclsopn  24171  cnfcf  24199  isclmp  25256  isncvsngp  25308  caucfil  25442  ovolgelb  25639  dyadmax  25757  ftc1a  26196  ulmcau  26558  noetasuplem4  27900  conway  27972  cofcutr  28117  addsprop  28169  onsfi  28549  perpcom  28993  colinearalg  29260  uhgrvd00  29884  pthdlem2lem  30116  frgrwopregbsn  30668  phoeqi  31209  ho02i  32181  hoeq2  32183  adjsym  32185  cnvadj  32244  mddmd2  32661  cdj3lem3b  32792  mgccnv  33319  cvmlift2lem12  35806  elpotr  36271  nmulcom  36686  fvineqsnf1  38076  poimirlem29  38320  heicant  38326  disjimeceqim  39473  ispsubsp2  40540  fsuppind  43342  nla0003  44171  ntrclsiso  44813  ntrneiiso  44837  ntrneik2  44838  ntrneix2  44839  ntrneik3  44842  ntrneix3  44843  ntrneik13  44844  ntrneix13  44845  ntrneik4w  44846  imo72b2  44918  tratrb  45265  hbra2VD  45588  tratrbVD  45589  termopropd  50042