Theorem ralcom 2828

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 2540	. 2 |- F/_ y A
2		nfcv 2540	. 2 |- F/_ x B
3	1, 2	ralcomf 2826	1 |- ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )

Syntax hints:   <-> wb 177   A.wral 2666

This theorem is referenced by:  ralcom4  2934  ssint  4026  iinrab2  4114  disjxun  4170  reusv3  4690  cnvpo  5369  cnvso  5370  fununi  5476  isocnv2  6010  dfsmo2  6568  ixpiin  7047  boxriin  7063  rexfiuz  12106  gcdcllem1  12966  mreacs  13838  comfeq  13887  catpropd  13890  isnsg2  14925  cntzrec  15087  oppgsubm  15113  opprirred  15762  opprsubrg  15844  tgss2  17007  ist1-2  17365  kgencn  17541  ptcnplem  17606  cnmptcom  17663  fbun  17825  cnflf  17987  fclsopn  17999  cnfcf  18027  caucfil  19189  ovolgelb  19329  dyadmax  19443  ftc1a  19874  ulmcau  20264  phoeqi  22312  ho02i  23285  hoeq2  23287  adjsym  23289  cnvadj  23348  mddmd2  23765  cdj3lem3b  23896  cvmlift2lem12  24954  dedekind  25140  dfpo2  25326  elpotr  25351  colinearalg  25753  islindf4  27176  2reu4a  27834  frgrawopreg2  28154  hbra2VD  28681  ispsubsp2  30228

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671