Theorem ralcom 3098

Description: Commutation of restricted universal quantifiers. See ralcom2 3104 for a version without DV condition on x , y. (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 2764	. 2 |- F/_ y A
2		nfcv 2764	. 2 |- F/_ x B
3	1, 2	ralcomf 3096	1 |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )

Syntax hints:   <-> wb 196   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  ralcom13  3100  ralrot3  3102  ralcom4  3224  ssint  4493  iinrab2  4583  disjxun  4651  reusv3  4876  cnvpo  5673  cnvso  5674  fununi  5964  isocnv2  6581  dfsmo2  7444  ixpiin  7934  boxriin  7950  dedekind  10200  rexfiuz  14087  gcdcllem1  15221  mreacs  16319  comfeq  16366  catpropd  16369  isnsg2  17624  cntzrec  17766  oppgsubm  17792  opprirred  18702  opprsubrg  18801  rmodislmodlem  18930  rmodislmod  18931  islindf4  20177  cpmatmcllem  20523  tgss2  20791  ist1-2  21151  kgencn  21359  ptcnplem  21424  cnmptcom  21481  fbun  21644  cnflf  21806  fclsopn  21818  cnfcf  21846  isclmp  22897  isncvsngp  22949  caucfil  23081  ovolgelb  23248  dyadmax  23366  ftc1a  23800  ulmcau  24149  perpcom  25608  colinearalg  25790  uhgrvd00  26430  pthdlem2lem  26663  frgrwopregbsn  27181  phoeqi  27713  ho02i  28688  hoeq2  28690  adjsym  28692  cnvadj  28751  mddmd2  29168  cdj3lem3b  29299  cvmlift2lem12  31296  dfpo2  31645  elpotr  31686  noetalem3  31865  conway  31910  poimirlem29  33438  heicant  33444  ispsubsp2  35032  ntrclsiso  38365  ntrneiiso  38389  ntrneik2  38390  ntrneix2  38391  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  ntrneik4w  38398  hbra2VD  39096  2reu4a  41189