Theorem ralcom 2950

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 2591	. 2 |- F/_ y A
2		nfcv 2591	. 2 |- F/_ x B
3	1, 2	ralcomf 2948	1 |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )

Syntax hints:   <-> wb 188   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1663  df-nf 1667  df-sb 1797  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741

This theorem is referenced by:  ralcom4  3065  ssint  4249  iinrab2  4340  disjxun  4399  reusv3  4610  cnvpo  5373  cnvso  5374  fununi  5647  isocnv2  6220  dfsmo2  7063  ixpiin  7545  boxriin  7561  dedekind  9794  rexfiuz  13403  gcdcllem1  14466  mreacs  15557  comfeq  15604  catpropd  15607  isnsg2  16840  cntzrec  16980  oppgsubm  17006  opprirred  17923  opprsubrg  18022  islindf4  19389  cpmatmcllem  19735  tgss2  19996  ist1-2  20356  kgencn  20564  ptcnplem  20629  cnmptcom  20686  fbun  20848  cnflf  21010  fclsopn  21022  cnfcf  21050  caucfil  22246  ovolgelb  22426  dyadmax  22549  ftc1a  22982  ulmcau  23343  perpcom  24751  colinearalg  24933  frgrawopreg2  25772  phoeqi  26492  ho02i  27475  hoeq2  27477  adjsym  27479  cnvadj  27538  mddmd2  27955  cdj3lem3b  28086  cvmlift2lem12  30030  dfpo2  30388  elpotr  30420  poimirlem29  31962  heicant  31968  ispsubsp2  33305  hbra2VD  37251  2reu4a  38604  uhgrvd00  39554