Theorem ralcom 3290

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1558   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-11 2191

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-ral 3077

This theorem is referenced by:  rexcom  3291  ralrot3  3293  ralcom13  3294  2reu4lem  4477  ssint  4922  iinrab2  5027  disjxun  5098  reusv3  5362  cnvpo  6274  cnvso  6275  dfpo2  6283  fununi  6596  isocnv2  7315  dfsmo2  8318  tz7.48lem  8412  ixpiin  8906  boxriin  8922  dedekind  11346  rexfiuz  15375  gcdcllem1  16533  mreacs  17690  comfeq  17738  catpropd  17741  isnsg2  19197  cntzrec  19376  oppgsubm  19402  opprirred  20471  opprsubrng  20609  opprsubrg  20643  opprdomnb  20767  rmodislmodlem  20996  rmodislmod  20997  islindf4  21890  cpmatmcllem  22778  tgss2  23047  ist1-2  23407  kgencn  23616  ptcnplem  23681  cnmptcom  23738  fbun  23900  cnflf  24062  fclsopn  24074  cnfcf  24102  isclmp  25159  isncvsngp  25211  caucfil  25345  ovolgelb  25542  dyadmax  25660  ftc1a  26099  ulmcau  26458  noetasuplem4  27800  conway  27872  cofcutr  28017  addsprop  28069  onsfi  28449  perpcom  28886  colinearalg  29111  uhgrvd00  29735  pthdlem2lem  29967  frgrwopregbsn  30519  phoeqi  31060  ho02i  32032  hoeq2  32034  adjsym  32036  cnvadj  32095  mddmd2  32512  cdj3lem3b  32643  mgccnv  33177  cvmlift2lem12  35664  elpotr  36129  nmulcom  36544  fvineqsnf1  37904  poimirlem29  38148  heicant  38154  disjimeceqim  39303  ispsubsp2  40370  fsuppind  43172  nla0003  44001  ntrclsiso  44643  ntrneiiso  44667  ntrneik2  44668  ntrneix2  44669  ntrneik3  44672  ntrneix3  44673  ntrneik13  44674  ntrneix13  44675  ntrneik4w  44676  imo72b2  44748  tratrb  45112  hbra2VD  45435  tratrbVD  45436  termopropd  49865