Theorem ralcom 3265

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3051

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 3052

This theorem is referenced by:  rexcom  3266  ralrot3  3268  ralcom13  3269  2reu4lem  4463  ssint  4906  iinrab2  5012  disjxun  5083  reusv3  5347  cnvpo  6251  cnvso  6252  dfpo2  6260  fununi  6573  isocnv2  7286  dfsmo2  8287  tz7.48lem  8380  ixpiin  8872  boxriin  8888  dedekind  11309  rexfiuz  15310  gcdcllem1  16468  mreacs  17624  comfeq  17672  catpropd  17675  isnsg2  19131  cntzrec  19311  oppgsubm  19337  opprirred  20402  opprsubrng  20536  opprsubrg  20570  opprdomnb  20694  rmodislmodlem  20924  rmodislmod  20925  islindf4  21818  cpmatmcllem  22683  tgss2  22952  ist1-2  23312  kgencn  23521  ptcnplem  23586  cnmptcom  23643  fbun  23805  cnflf  23967  fclsopn  23979  cnfcf  24007  isclmp  25064  isncvsngp  25116  caucfil  25250  ovolgelb  25447  dyadmax  25565  ftc1a  26004  ulmcau  26360  noetasuplem4  27700  conway  27771  cofcutr  27916  addsprop  27968  onsfi  28348  perpcom  28781  colinearalg  28979  uhgrvd00  29603  pthdlem2lem  29835  frgrwopregbsn  30387  phoeqi  30928  ho02i  31900  hoeq2  31902  adjsym  31904  cnvadj  31963  mddmd2  32380  cdj3lem3b  32511  mgccnv  33059  cvmlift2lem12  35496  elpotr  35961  fvineqsnf1  37726  poimirlem29  37970  heicant  37976  disjimeceqim  39125  ispsubsp2  40192  fsuppind  43023  nla0003  43852  ntrclsiso  44494  ntrneiiso  44518  ntrneik2  44519  ntrneix2  44520  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  ntrneik4w  44527  imo72b2  44599  tratrb  44963  hbra2VD  45286  tratrbVD  45287  termopropd  49719