Theorem ralcom 3267

Description: Commutation of restricted universal quantifiers. See ralcom2 3341 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3341 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 465	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
2	1	2albii 1827	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
3		alcom 2170	. . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
4	2, 3	bitri 276	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
5		r2al 3175	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3175	. 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
7	4, 5, 6	3bitr4i 304	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-11 2168

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054

This theorem is referenced by:  rexcom  3268  ralrot3  3270  ralcom13  3271  2reu4lem  4451  ssint  4894  iinrab2  4999  disjxun  5070  reusv3  5334  cnvpo  6238  cnvso  6239  dfpo2  6247  fununi  6560  isocnv2  7275  dfsmo2  8277  tz7.48lem  8370  ixpiin  8862  boxriin  8878  dedekind  11300  rexfiuz  15301  gcdcllem1  16459  mreacs  17615  comfeq  17663  catpropd  17666  isnsg2  19122  cntzrec  19302  oppgsubm  19328  opprirred  20393  opprsubrng  20531  opprsubrg  20565  opprdomnb  20689  rmodislmodlem  20919  rmodislmod  20920  islindf4  21813  cpmatmcllem  22701  tgss2  22970  ist1-2  23330  kgencn  23539  ptcnplem  23604  cnmptcom  23661  fbun  23823  cnflf  23985  fclsopn  23997  cnfcf  24025  isclmp  25082  isncvsngp  25134  caucfil  25268  ovolgelb  25465  dyadmax  25583  ftc1a  26022  ulmcau  26378  noetasuplem4  27718  conway  27789  cofcutr  27934  addsprop  27986  onsfi  28366  perpcom  28799  colinearalg  28997  uhgrvd00  29621  pthdlem2lem  29853  frgrwopregbsn  30405  phoeqi  30946  ho02i  31918  hoeq2  31920  adjsym  31922  cnvadj  31981  mddmd2  32398  cdj3lem3b  32529  mgccnv  33078  cvmlift2lem12  35542  elpotr  36007  fvineqsnf1  37772  poimirlem29  38016  heicant  38022  disjimeceqim  39171  ispsubsp2  40238  fsuppind  43040  nla0003  43869  ntrclsiso  44511  ntrneiiso  44535  ntrneik2  44536  ntrneix2  44537  ntrneik3  44540  ntrneix3  44541  ntrneik13  44542  ntrneix13  44543  ntrneik4w  44544  imo72b2  44616  tratrb  44980  hbra2VD  45303  tratrbVD  45304  termopropd  49734