Theorem ralcom 3307

Description: Commutation of restricted universal quantifiers. See ralcom2 3316 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3316 since it depends on a smaller set of axioms. (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		ancomst 468	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
2	1	2albii 1822	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
3		alcom 2160	. . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
5		r2al 3166	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3166	. 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-11 2158

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111

This theorem is referenced by:  ralcom13  3312  ralrot3  3314  ralcom4OLD  3472  2reu4lem  4423  ssint  4854  iinrab2  4955  disjxun  5028  reusv3  5271  cnvpo  6106  cnvso  6107  fununi  6399  isocnv2  7063  dfsmo2  7967  tz7.48lem  8060  ixpiin  8471  boxriin  8487  dedekind  10792  rexfiuz  14699  gcdcllem1  15838  mreacs  16921  comfeq  16968  catpropd  16971  isnsg2  18300  cntzrec  18456  oppgsubm  18482  opprirred  19448  opprsubrg  19549  rmodislmodlem  19694  rmodislmod  19695  islindf4  20527  cpmatmcllem  21323  tgss2  21592  ist1-2  21952  kgencn  22161  ptcnplem  22226  cnmptcom  22283  fbun  22445  cnflf  22607  fclsopn  22619  cnfcf  22647  isclmp  23702  isncvsngp  23754  caucfil  23887  ovolgelb  24084  dyadmax  24202  ftc1a  24640  ulmcau  24990  perpcom  26507  colinearalg  26704  uhgrvd00  27324  pthdlem2lem  27556  frgrwopregbsn  28102  phoeqi  28640  ho02i  29612  hoeq2  29614  adjsym  29616  cnvadj  29675  mddmd2  30092  cdj3lem3b  30223  mcgcnv  30705  cvmlift2lem12  32674  dfpo2  33104  elpotr  33139  noetalem3  33332  conway  33377  fvineqsnf1  34827  poimirlem29  35086  heicant  35092  ispsubsp2  37042  fsuppind  39456  ntrclsiso  40770  ntrneiiso  40794  ntrneik2  40795  ntrneix2  40796  ntrneik3  40799  ntrneix3  40800  ntrneik13  40801  ntrneix13  40802  ntrneik4w  40803  imo72b2  40878  tratrb  41242  hbra2VD  41566  tratrbVD  41567