Theorem ralcom 3002

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 2603	. 2 |- F/_ y A
2		nfcv 2603	. 2 |- F/_ x B
3	1, 2	ralcomf 3000	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 2791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1598  df-nf 1602  df-sb 1725  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796

This theorem is referenced by:  ralcom4  3112  ssint  4283  iinrab2  4374  disjxun  4431  reusv3  4641  cnvpo  5531  cnvso  5532  fununi  5640  isocnv2  6208  dfsmo2  7016  ixpiin  7493  boxriin  7509  dedekind  9742  rexfiuz  13154  gcdcllem1  14021  mreacs  14927  comfeq  14973  catpropd  14976  isnsg2  16100  cntzrec  16240  oppgsubm  16266  opprirred  17219  opprsubrg  17318  islindf4  18740  cpmatmcllem  19086  tgss2  19355  ist1-2  19714  kgencn  19923  ptcnplem  19988  cnmptcom  20045  fbun  20207  cnflf  20369  fclsopn  20381  cnfcf  20409  caucfil  21588  ovolgelb  21757  dyadmax  21873  ftc1a  22304  ulmcau  22655  perpcom  23955  colinearalg  24078  frgrawopreg2  24916  phoeqi  25638  ho02i  26613  hoeq2  26615  adjsym  26617  cnvadj  26676  mddmd2  27093  cdj3lem3b  27224  cvmlift2lem12  28625  dfpo2  29152  elpotr  29181  heicant  30017  2reu4a  32028  hbra2VD  33368  ispsubsp2  35172