Theorem ralcom 2979

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 2613	. 2 |- F/_ y A
2		nfcv 2613	. 2 |- F/_ x B
3	1, 2	ralcomf 2977	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 2795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1588  df-nf 1591  df-sb 1703  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800

This theorem is referenced by:  ralcom4  3089  ssint  4244  iinrab2  4333  disjxun  4390  reusv3  4600  cnvpo  5475  cnvso  5476  fununi  5584  isocnv2  6123  dfsmo2  6910  ixpiin  7391  boxriin  7407  dedekind  9636  rexfiuz  12939  gcdcllem1  13799  mreacs  14700  comfeq  14749  catpropd  14752  isnsg2  15815  cntzrec  15955  oppgsubm  15981  opprirred  16902  opprsubrg  16994  islindf4  18378  tgss2  18710  ist1-2  19069  kgencn  19247  ptcnplem  19312  cnmptcom  19369  fbun  19531  cnflf  19693  fclsopn  19705  cnfcf  19733  caucfil  20912  ovolgelb  21081  dyadmax  21196  ftc1a  21627  ulmcau  21978  perpcom  23234  colinearalg  23293  phoeqi  24395  ho02i  25370  hoeq2  25372  adjsym  25374  cnvadj  25433  mddmd2  25850  cdj3lem3b  25981  cvmlift2lem12  27339  dfpo2  27701  elpotr  27730  heicant  28566  2reu4a  30153  frgrawopreg2  30784  cpmatmcllem  31183  hbra2VD  31898  ispsubsp2  33698