Theorem ralcom 3167

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   ∈ wcel 2107  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-11 2155

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3070

This theorem is referenced by:  rexcom  3235  ralcom13  3287  ralrot3  3289  2reu4lem  4457  ssint  4896  iinrab2  5000  disjxun  5073  reusv3  5329  cnvpo  6194  cnvso  6195  dfpo2  6203  fununi  6516  isocnv2  7211  dfsmo2  8187  tz7.48lem  8281  ixpiin  8721  boxriin  8737  dedekind  11147  rexfiuz  15068  gcdcllem1  16215  mreacs  17376  comfeq  17424  catpropd  17427  isnsg2  18793  cntzrec  18949  oppgsubm  18978  opprirred  19953  opprsubrg  20054  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  islindf4  21054  cpmatmcllem  21876  tgss2  22146  ist1-2  22507  kgencn  22716  ptcnplem  22781  cnmptcom  22838  fbun  23000  cnflf  23162  fclsopn  23174  cnfcf  23202  isclmp  24269  isncvsngp  24322  caucfil  24456  ovolgelb  24653  dyadmax  24771  ftc1a  25210  ulmcau  25563  perpcom  27083  colinearalg  27287  uhgrvd00  27910  pthdlem2lem  28144  frgrwopregbsn  28690  phoeqi  29228  ho02i  30200  hoeq2  30202  adjsym  30204  cnvadj  30263  mddmd2  30680  cdj3lem3b  30811  mgccnv  31286  cvmlift2lem12  33285  elpotr  33766  noetasuplem4  33948  conway  34002  cofcutr  34101  fvineqsnf1  35590  poimirlem29  35815  heicant  35821  ispsubsp2  37767  fsuppind  40286  ntrclsiso  41684  ntrneiiso  41708  ntrneik2  41709  ntrneix2  41710  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  ntrneik4w  41717  imo72b2  41790  tratrb  42163  hbra2VD  42487  tratrbVD  42488