Theorem ralcom 2876

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 2574	. 2 |- F/_ y A
2		nfcv 2574	. 2 |- F/_ x B
3	1, 2	ralcomf 2874	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 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715

This theorem is referenced by:  ralcom4  2986  ssint  4139  iinrab2  4228  disjxun  4285  reusv3  4495  cnvpo  5370  cnvso  5371  fununi  5479  isocnv2  6017  dfsmo2  6800  ixpiin  7281  boxriin  7297  dedekind  9525  rexfiuz  12827  gcdcllem1  13687  mreacs  14588  comfeq  14637  catpropd  14640  isnsg2  15702  cntzrec  15842  oppgsubm  15868  opprirred  16784  opprsubrg  16866  islindf4  18247  tgss2  18572  ist1-2  18931  kgencn  19109  ptcnplem  19174  cnmptcom  19231  fbun  19393  cnflf  19555  fclsopn  19567  cnfcf  19595  caucfil  20774  ovolgelb  20943  dyadmax  21058  ftc1a  21489  ulmcau  21840  perpcom  23080  colinearalg  23124  phoeqi  24226  ho02i  25201  hoeq2  25203  adjsym  25205  cnvadj  25264  mddmd2  25681  cdj3lem3b  25812  cvmlift2lem12  27172  dfpo2  27534  elpotr  27563  heicant  28397  2reu4a  29984  frgrawopreg2  30615  hbra2VD  31525  ispsubsp2  33283