Theorem ralcom 3018

Description: Commutation of restricted universal quantifiers. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
ralcom	|- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )

Distinct variable groups:   x, y   x, B   y, A

Allowed substitution hints:   ph( x, y)   A( x)   B( y)

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		nfcv 2619	. 2 |- F/_ y A
2		nfcv 2619	. 2 |- F/_ x B
3	1, 2	ralcomf 3016	1 |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )

Syntax hints:   <-> wb 184   A.wral 2807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1614  df-nf 1618  df-sb 1741  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812

This theorem is referenced by:  ralcom4  3128  ssint  4304  iinrab2  4395  disjxun  4454  reusv3  4664  cnvpo  5551  cnvso  5552  fununi  5660  isocnv2  6228  dfsmo2  7036  ixpiin  7514  boxriin  7530  dedekind  9761  rexfiuz  13192  gcdcllem1  14161  mreacs  15075  comfeq  15122  catpropd  15125  isnsg2  16358  cntzrec  16498  oppgsubm  16524  opprirred  17478  opprsubrg  17577  islindf4  19000  cpmatmcllem  19346  tgss2  19616  ist1-2  19975  kgencn  20183  ptcnplem  20248  cnmptcom  20305  fbun  20467  cnflf  20629  fclsopn  20641  cnfcf  20669  caucfil  21848  ovolgelb  22017  dyadmax  22133  ftc1a  22564  ulmcau  22916  perpcom  24216  colinearalg  24340  frgrawopreg2  25178  phoeqi  25900  ho02i  26875  hoeq2  26877  adjsym  26879  cnvadj  26938  mddmd2  27355  cdj3lem3b  27486  cvmlift2lem12  28956  dfpo2  29402  elpotr  29430  heicant  30254  2reu4a  32397  hbra2VD  33803  ispsubsp2  35613