MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralcom Structured version   Visualization version   GIF version

Theorem ralcom 3284
Description: Commutation of restricted universal quantifiers. See ralcom2 3371 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3371 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
StepHypRef Expression
1 ancomst 463 . . . 4 (((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ((𝑦𝐵𝑥𝐴) → 𝜑))
212albii 1814 . . 3 (∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ∀𝑥𝑦((𝑦𝐵𝑥𝐴) → 𝜑))
3 alcom 2148 . . 3 (∀𝑥𝑦((𝑦𝐵𝑥𝐴) → 𝜑) ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
42, 3bitri 274 . 2 (∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
5 r2al 3192 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
6 r2al 3192 . 2 (∀𝑦𝐵𝑥𝐴 𝜑 ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
74, 5, 63bitr4i 302 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1531  wcel 2098  wral 3058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-11 2146
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-ral 3059
This theorem is referenced by:  rexcom  3285  ralrot3  3288  ralcom13  3289  ralcom13OLD  3290  2reu4lem  4529  ssint  4971  iinrab2  5077  disjxun  5150  reusv3  5409  cnvpo  6296  cnvso  6297  dfpo2  6305  fununi  6633  isocnv2  7345  dfsmo2  8374  tz7.48lem  8468  ixpiin  8949  boxriin  8965  dedekind  11415  rexfiuz  15334  gcdcllem1  16481  mreacs  17645  comfeq  17693  catpropd  17696  isnsg2  19118  cntzrec  19294  oppgsubm  19323  opprirred  20368  opprsubrng  20503  opprsubrg  20539  rmodislmodlem  20819  rmodislmod  20820  rmodislmodOLD  20821  islindf4  21779  cpmatmcllem  22640  tgss2  22910  ist1-2  23271  kgencn  23480  ptcnplem  23545  cnmptcom  23602  fbun  23764  cnflf  23926  fclsopn  23938  cnfcf  23966  isclmp  25044  isncvsngp  25097  caucfil  25231  ovolgelb  25429  dyadmax  25547  ftc1a  25992  ulmcau  26351  noetasuplem4  27689  conway  27752  cofcutr  27864  addsprop  27913  perpcom  28537  colinearalg  28741  uhgrvd00  29368  pthdlem2lem  29601  frgrwopregbsn  30147  phoeqi  30687  ho02i  31659  hoeq2  31661  adjsym  31663  cnvadj  31722  mddmd2  32139  cdj3lem3b  32270  mgccnv  32747  cvmlift2lem12  34957  elpotr  35410  fvineqsnf1  36922  poimirlem29  37155  heicant  37161  ispsubsp2  39251  fsuppind  41854  nla0003  42886  ntrclsiso  43528  ntrneiiso  43552  ntrneik2  43553  ntrneix2  43554  ntrneik3  43557  ntrneix3  43558  ntrneik13  43559  ntrneix13  43560  ntrneik4w  43561  imo72b2  43633  tratrb  44006  hbra2VD  44330  tratrbVD  44331
  Copyright terms: Public domain W3C validator