Theorem ralcom 3260

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2160

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048

This theorem is referenced by:  rexcom  3261  ralrot3  3263  ralcom13  3264  2reu4lem  4469  ssint  4912  iinrab2  5016  disjxun  5087  reusv3  5341  cnvpo  6234  cnvso  6235  dfpo2  6243  fununi  6556  isocnv2  7265  dfsmo2  8267  tz7.48lem  8360  ixpiin  8848  boxriin  8864  dedekind  11276  rexfiuz  15255  gcdcllem1  16410  mreacs  17564  comfeq  17612  catpropd  17615  isnsg2  19068  cntzrec  19248  oppgsubm  19274  opprirred  20340  opprsubrng  20474  opprsubrg  20508  opprdomnb  20632  rmodislmodlem  20862  rmodislmod  20863  islindf4  21775  cpmatmcllem  22633  tgss2  22902  ist1-2  23262  kgencn  23471  ptcnplem  23536  cnmptcom  23593  fbun  23755  cnflf  23917  fclsopn  23929  cnfcf  23957  isclmp  25024  isncvsngp  25076  caucfil  25210  ovolgelb  25408  dyadmax  25526  ftc1a  25971  ulmcau  26331  noetasuplem4  27675  conway  27740  cofcutr  27868  addsprop  27919  onsfi  28283  perpcom  28691  colinearalg  28888  uhgrvd00  29513  pthdlem2lem  29745  frgrwopregbsn  30297  phoeqi  30837  ho02i  31809  hoeq2  31811  adjsym  31813  cnvadj  31872  mddmd2  32289  cdj3lem3b  32420  mgccnv  32980  cvmlift2lem12  35358  elpotr  35823  fvineqsnf1  37454  poimirlem29  37699  heicant  37705  ispsubsp2  39855  fsuppind  42693  nla0003  43528  ntrclsiso  44170  ntrneiiso  44194  ntrneik2  44195  ntrneix2  44196  ntrneik3  44199  ntrneix3  44200  ntrneik13  44201  ntrneix13  44202  ntrneik4w  44203  imo72b2  44275  tratrb  44639  hbra2VD  44962  tratrbVD  44963  termopropd  49355