Theorem ralcom 2871

Description: Commutation of restricted 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 2569	. 2 |- F/_ y A
2		nfcv 2569	. 2 |- F/_ x B
3	1, 2	ralcomf 2869	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 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710

This theorem is referenced by:  ralcom4  2981  ssint  4132  iinrab2  4221  disjxun  4278  reusv3  4488  cnvpo  5363  cnvso  5364  fununi  5472  isocnv2  6009  dfsmo2  6794  ixpiin  7277  boxriin  7293  dedekind  9520  rexfiuz  12818  gcdcllem1  13677  mreacs  14578  comfeq  14627  catpropd  14630  isnsg2  15690  cntzrec  15830  oppgsubm  15856  opprirred  16727  opprsubrg  16809  islindf4  18108  tgss2  18433  ist1-2  18792  kgencn  18970  ptcnplem  19035  cnmptcom  19092  fbun  19254  cnflf  19416  fclsopn  19428  cnfcf  19456  caucfil  20635  ovolgelb  20804  dyadmax  20919  ftc1a  21350  ulmcau  21744  colinearalg  22978  phoeqi  24080  ho02i  25055  hoeq2  25057  adjsym  25059  cnvadj  25118  mddmd2  25535  cdj3lem3b  25666  cvmlift2lem12  27050  dfpo2  27411  elpotr  27440  heicant  28267  2reu4a  29856  frgrawopreg2  30487  hbra2VD  31295  ispsubsp2  32960