Theorem ralcom 3295

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2146  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-11 2195

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3082

This theorem is used by:  rexcom  3296  ralrot3  3298  ralcom13  3299  2reu4lem  4486  ssint  4931  iinrab2  5036  disjxun  5109  reusv3  5378  cnvpo  6292  cnvso  6293  dfpo2  6301  fununi  6615  isocnv2  7338  dfsmo2  8340  tz7.48lem  8434  ixpiin  8928  boxriin  8944  dedekind  11390  rexfiuz  15425  gcdcllem1  16581  mreacs  17738  comfeq  17786  catpropd  17789  isnsg2  19268  cntzrec  19452  oppgsubm  19478  opprirred  20552  opprsubrng  20710  opprsubrg  20744  opprdomnb  20867  rmodislmodlem  21102  rmodislmod  21103  islindf4  22040  cpmatmcllem  22927  tgss2  23196  ist1-2  23556  kgencn  23766  ptcnplem  23831  cnmptcom  23888  fbun  24050  cnflf  24212  fclsopn  24224  cnfcf  24252  isclmp  25309  isncvsngp  25361  caucfil  25495  ovolgelb  25692  dyadmax  25810  ftc1a  26249  ulmcau  26611  noetasuplem4  27953  conway  28025  cofcutr  28170  addsprop  28222  onsfi  28602  perpcom  29046  colinearalg  29317  uhgrvd00  29944  pthdlem2lem  30182  frgrwopregbsn  30741  phoeqi  31282  ho02i  32254  hoeq2  32256  adjsym  32258  cnvadj  32317  mddmd2  32734  cdj3lem3b  32865  mgccnv  33385  cvmlift2lem12  35845  elpotr  36310  nmulcom  36725  fvineqsnf1  38115  poimirlem29  38359  heicant  38365  disjimeceqim  39513  ispsubsp2  40580  fsuppind  43382  nla0003  44211  ntrclsiso  44853  ntrneiiso  44877  ntrneik2  44878  ntrneix2  44879  ntrneik3  44882  ntrneix3  44883  ntrneik13  44884  ntrneix13  44885  ntrneik4w  44886  imo72b2  44958  tratrb  45305  hbra2VD  45628  tratrbVD  45629  termopropd  50081