Theorem ralcom 3266

Description: Commutation of restricted universal quantifiers. See ralcom2 3349 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3349 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  4478  ssint  4921  iinrab2  5027  disjxun  5098  reusv3  5352  cnvpo  6253  cnvso  6254  dfpo2  6262  fununi  6575  isocnv2  7287  dfsmo2  8289  tz7.48lem  8382  ixpiin  8874  boxriin  8890  dedekind  11308  rexfiuz  15283  gcdcllem1  16438  mreacs  17593  comfeq  17641  catpropd  17644  isnsg2  19097  cntzrec  19277  oppgsubm  19303  opprirred  20370  opprsubrng  20504  opprsubrg  20538  opprdomnb  20662  rmodislmodlem  20892  rmodislmod  20893  islindf4  21805  cpmatmcllem  22674  tgss2  22943  ist1-2  23303  kgencn  23512  ptcnplem  23577  cnmptcom  23634  fbun  23796  cnflf  23958  fclsopn  23970  cnfcf  23998  isclmp  25065  isncvsngp  25117  caucfil  25251  ovolgelb  25449  dyadmax  25567  ftc1a  26012  ulmcau  26372  noetasuplem4  27716  conway  27787  cofcutr  27932  addsprop  27984  onsfi  28364  perpcom  28797  colinearalg  28995  uhgrvd00  29620  pthdlem2lem  29852  frgrwopregbsn  30404  phoeqi  30945  ho02i  31917  hoeq2  31919  adjsym  31921  cnvadj  31980  mddmd2  32397  cdj3lem3b  32528  mgccnv  33092  cvmlift2lem12  35530  elpotr  35995  fvineqsnf1  37665  poimirlem29  37900  heicant  37906  disjimeceqim  39055  ispsubsp2  40122  fsuppind  42948  nla0003  43781  ntrclsiso  44423  ntrneiiso  44447  ntrneik2  44448  ntrneix2  44449  ntrneik3  44452  ntrneix3  44453  ntrneik13  44454  ntrneix13  44455  ntrneik4w  44456  imo72b2  44528  tratrb  44892  hbra2VD  45215  tratrbVD  45216  termopropd  49603