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  14501  gcdcllem1  15637  mreacs  16715  comfeq  16762  catpropd  16765  isnsg2  18019  cntzrec  18160  oppgsubm  18186  opprirred  19100  opprsubrg  19204  rmodislmodlem  19333  rmodislmod  19334  islindf4  20592  cpmatmcllem  20941  tgss2  21210  ist1-2  21570  kgencn  21779  ptcnplem  21844  cnmptcom  21901  fbun  22063  cnflf  22225  fclsopn  22237  cnfcf  22265  isclmp  23315  isncvsngp  23367  caucfil  23500  ovolgelb  23695  dyadmax  23813  ftc1a  24248  ulmcau  24597  perpcom  26081  colinearalg  26276  uhgrvd00  26899  pthdlem2lem  27136  frgrwopregbsn  27742  phoeqi  28302  ho02i  29277  hoeq2  29279  adjsym  29281  cnvadj  29340  mddmd2  29757  cdj3lem3b  29888  cvmlift2lem12  31903  dfpo2  32247  elpotr  32282  noetalem3  32462  conway  32507  poimirlem29  34073  heicant  34079  ispsubsp2  35909  ntrclsiso  39335  ntrneiiso  39359  ntrneik2  39360  ntrneix2  39361  ntrneik3  39364  ntrneix3  39365  ntrneik13  39366  ntrneix13  39367  ntrneik4w  39368  hbra2VD  40043  2reu4a  42164