Theorem ralcom 3266

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3052

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 1912  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053

This theorem is referenced by:  rexcom  3267  ralrot3  3269  ralcom13  3270  2reu4lem  4464  ssint  4907  iinrab2  5013  disjxun  5084  reusv3  5343  cnvpo  6246  cnvso  6247  dfpo2  6255  fununi  6568  isocnv2  7280  dfsmo2  8281  tz7.48lem  8374  ixpiin  8866  boxriin  8882  dedekind  11303  rexfiuz  15304  gcdcllem1  16462  mreacs  17618  comfeq  17666  catpropd  17669  isnsg2  19125  cntzrec  19305  oppgsubm  19331  opprirred  20396  opprsubrng  20530  opprsubrg  20564  opprdomnb  20688  rmodislmodlem  20918  rmodislmod  20919  islindf4  21831  cpmatmcllem  22696  tgss2  22965  ist1-2  23325  kgencn  23534  ptcnplem  23599  cnmptcom  23656  fbun  23818  cnflf  23980  fclsopn  23992  cnfcf  24020  isclmp  25077  isncvsngp  25129  caucfil  25263  ovolgelb  25460  dyadmax  25578  ftc1a  26017  ulmcau  26376  noetasuplem4  27717  conway  27788  cofcutr  27933  addsprop  27985  onsfi  28365  perpcom  28798  colinearalg  28996  uhgrvd00  29621  pthdlem2lem  29853  frgrwopregbsn  30405  phoeqi  30946  ho02i  31918  hoeq2  31920  adjsym  31922  cnvadj  31981  mddmd2  32398  cdj3lem3b  32529  mgccnv  33077  cvmlift2lem12  35515  elpotr  35980  fvineqsnf1  37743  poimirlem29  37987  heicant  37993  disjimeceqim  39142  ispsubsp2  40209  fsuppind  43040  nla0003  43873  ntrclsiso  44515  ntrneiiso  44539  ntrneik2  44540  ntrneix2  44541  ntrneik3  44544  ntrneix3  44545  ntrneik13  44546  ntrneix13  44547  ntrneik4w  44548  imo72b2  44620  tratrb  44984  hbra2VD  45307  tratrbVD  45308  termopropd  49734