Theorem ralcom 3284

Description: Commutation of restricted universal quantifiers. See ralcom2 3290 for a version without disjoint variable condition on 𝑥, 𝑦. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
ralcom	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐵   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		nfcv 2934	. 2 ⊢ Ⅎ𝑦𝐴
2		nfcv 2934	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	ralcomf 3282	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 198  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clel 2774  df-nfc 2921  df-ral 3095

This theorem is referenced by:  ralcom13  3286  ralrot3  3288  ralcom4  3426  ssint  4728  iinrab2  4818  disjxun  4886  reusv3  5119  cnvpo  5929  cnvso  5930  fununi  6211  isocnv2  6855  dfsmo2  7729  ixpiin  8222  boxriin  8238  dedekind  10541  rexfiuz  14498  gcdcllem1  15631  mreacs  16708  comfeq  16755  catpropd  16758  isnsg2  18012  cntzrec  18153  oppgsubm  18179  opprirred  19093  opprsubrg  19197  rmodislmodlem  19326  rmodislmod  19327  islindf4  20585  cpmatmcllem  20934  tgss2  21203  ist1-2  21563  kgencn  21772  ptcnplem  21837  cnmptcom  21894  fbun  22056  cnflf  22218  fclsopn  22230  cnfcf  22258  isclmp  23308  isncvsngp  23360  caucfil  23493  ovolgelb  23688  dyadmax  23806  ftc1a  24241  ulmcau  24590  perpcom  26068  colinearalg  26263  uhgrvd00  26886  pthdlem2lem  27123  frgrwopregbsn  27729  phoeqi  28289  ho02i  29264  hoeq2  29266  adjsym  29268  cnvadj  29327  mddmd2  29744  cdj3lem3b  29875  cvmlift2lem12  31899  dfpo2  32243  elpotr  32278  noetalem3  32458  conway  32503  poimirlem29  34069  heicant  34075  ispsubsp2  35905  ntrclsiso  39331  ntrneiiso  39355  ntrneik2  39356  ntrneix2  39357  ntrneik3  39360  ntrneix3  39361  ntrneik13  39362  ntrneix13  39363  ntrneik4w  39364  hbra2VD  40039  2reu4a  42160