Theorem ralcom 3018

Description: Commutation of restricted universal quantifiers. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
ralcom

Distinct variable groups:   ,   ,   ,

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		nfcv 2619	. 2
2		nfcv 2619	. 2
3	1, 2	ralcomf 3016	1

Syntax hints:  <->wb 184  A.wral 2807

This theorem is referenced by:  ralcom4  3128  ssint  4302  iinrab2  4393  disjxun  4450  reusv3  4660  cnvpo  5550  cnvso  5551  fununi  5659  isocnv2  6227  dfsmo2  7037  ixpiin  7515  boxriin  7531  dedekind  9765  rexfiuz  13180  gcdcllem1  14149  mreacs  15055  comfeq  15101  catpropd  15104  isnsg2  16231  cntzrec  16371  oppgsubm  16397  opprirred  17351  opprsubrg  17450  islindf4  18873  cpmatmcllem  19219  tgss2  19489  ist1-2  19848  kgencn  20057  ptcnplem  20122  cnmptcom  20179  fbun  20341  cnflf  20503  fclsopn  20515  cnfcf  20543  caucfil  21722  ovolgelb  21891  dyadmax  22007  ftc1a  22438  ulmcau  22790  perpcom  24090  colinearalg  24213  frgrawopreg2  25051  phoeqi  25773  ho02i  26748  hoeq2  26750  adjsym  26752  cnvadj  26811  mddmd2  27228  cdj3lem3b  27359  cvmlift2lem12  28759  dfpo2  29184  elpotr  29213  heicant  30049  2reu4a  32194  hbra2VD  33660  ispsubsp2  35470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812