Theorem ralcom 3291

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

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

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 2194

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

This theorem is used by:  rexcom  3292  ralrot3  3294  ralcom13  3295  2reu4lem  4479  ssint  4924  iinrab2  5028  disjxun  5101  reusv3  5367  cnvpo  6290  cnvso  6291  dfpo2  6299  fununi  6615  isocnv2  7339  dfsmo2  8355  tz7.48lemOLD  8451  ixpiin  8952  boxriin  8968  dedekind  11473  rexfiuz  15515  gcdcllem1  16669  mreacs  17832  comfeq  17880  catpropd  17883  isnsg2  19366  cntzrec  19550  oppgsubm  19576  opprirred  20652  opprsubrng  20811  opprsubrg  20845  opprdomnb  20968  rmodislmodlem  21204  rmodislmod  21205  islindf4  22144  cpmatmcllem  23036  tgss2  23305  ist1-2  23665  kgencn  23875  ptcnplem  23940  cnmptcom  23997  fbun  24159  cnflf  24321  fclsopn  24333  cnfcf  24361  isclmp  25418  isncvsngp  25470  caucfil  25604  ovolgelb  25801  dyadmax  25919  ftc1a  26357  ulmcau  26722  noetasuplem4  28093  conway  28165  cofcutr  28310  addsprop  28362  onsfi  28742  perpcom  29188  colinearalg  29488  uhgrvd00  30115  pthdlem2lem  30353  frgrwopregbsn  30918  phoeqi  31459  ho02i  32431  hoeq2  32433  adjsym  32435  cnvadj  32494  mddmd2  32911  cdj3lem3b  33042  mgccnv  33560  cvmlift2lem12  36079  elpotr  36543  nmulcom  36943  fvineqsnf1  38333  poimirlem29  38567  heicant  38573  disjimeceqim  39736  ispsubsp2  40803  fsuppind  43618  nla0003  44425  ntrclsiso  45066  ntrneiiso  45090  ntrneik2  45091  ntrneix2  45092  ntrneik3  45095  ntrneix3  45096  ntrneik13  45097  ntrneix13  45098  ntrneik4w  45099  imo72b2  45171  tratrb  45518  hbra2VD  45841  tratrbVD  45842  termopropd  50351