Theorem ralcom 2968

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 2564	. 2 |- F/_ y A
2		nfcv 2564	. 2 |- F/_ x B
3	1, 2	ralcomf 2966	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 2754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1634  df-nf 1638  df-sb 1764  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759

This theorem is referenced by:  ralcom4  3078  ssint  4243  iinrab2  4334  disjxun  4393  reusv3  4602  cnvpo  5362  cnvso  5363  fununi  5635  isocnv2  6210  dfsmo2  7051  ixpiin  7533  boxriin  7549  dedekind  9778  rexfiuz  13329  gcdcllem1  14358  mreacs  15272  comfeq  15319  catpropd  15322  isnsg2  16555  cntzrec  16695  oppgsubm  16721  opprirred  17671  opprsubrg  17770  islindf4  19165  cpmatmcllem  19511  tgss2  19781  ist1-2  20141  kgencn  20349  ptcnplem  20414  cnmptcom  20471  fbun  20633  cnflf  20795  fclsopn  20807  cnfcf  20835  caucfil  22014  ovolgelb  22183  dyadmax  22299  ftc1a  22730  ulmcau  23082  perpcom  24476  colinearalg  24630  frgrawopreg2  25468  phoeqi  26187  ho02i  27161  hoeq2  27163  adjsym  27165  cnvadj  27224  mddmd2  27641  cdj3lem3b  27772  cvmlift2lem12  29611  dfpo2  29968  elpotr  30000  heicant  31421  ispsubsp2  32763  hbra2VD  36691  2reu4a  37562