Theorem ralcom 3015

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 2622	. 2 |- F/_ y A
2		nfcv 2622	. 2 |- F/_ x B
3	1, 2	ralcomf 3013	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 2807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1707  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812

This theorem is referenced by:  ralcom4  3125  ssint  4291  iinrab2  4381  disjxun  4438  reusv3  4648  cnvpo  5536  cnvso  5537  fununi  5645  isocnv2  6206  dfsmo2  7008  ixpiin  7485  boxriin  7501  dedekind  9732  rexfiuz  13129  gcdcllem1  13997  mreacs  14902  comfeq  14951  catpropd  14954  isnsg2  16019  cntzrec  16159  oppgsubm  16185  opprirred  17128  opprsubrg  17226  islindf4  18633  cpmatmcllem  18979  tgss2  19248  ist1-2  19607  kgencn  19785  ptcnplem  19850  cnmptcom  19907  fbun  20069  cnflf  20231  fclsopn  20243  cnfcf  20271  caucfil  21450  ovolgelb  21619  dyadmax  21735  ftc1a  22166  ulmcau  22517  perpcom  23791  colinearalg  23882  phoeqi  25299  ho02i  26274  hoeq2  26276  adjsym  26278  cnvadj  26337  mddmd2  26754  cdj3lem3b  26885  cvmlift2lem12  28249  dfpo2  28611  elpotr  28640  heicant  29477  2reu4a  31480  frgrawopreg2  31770  hbra2VD  32615  ispsubsp2  34417