Theorem ralcom 3263

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  rexcom  3264  ralrot3  3266  ralcom13  3267  ralcom13OLD  3268  2reu4lem  4481  ssint  4924  iinrab2  5029  disjxun  5100  reusv3  5355  cnvpo  6248  cnvso  6249  dfpo2  6257  fununi  6575  isocnv2  7288  dfsmo2  8293  tz7.48lem  8386  ixpiin  8874  boxriin  8890  dedekind  11313  rexfiuz  15290  gcdcllem1  16445  mreacs  17599  comfeq  17647  catpropd  17650  isnsg2  19070  cntzrec  19250  oppgsubm  19276  opprirred  20342  opprsubrng  20479  opprsubrg  20513  opprdomnb  20637  rmodislmodlem  20867  rmodislmod  20868  islindf4  21780  cpmatmcllem  22638  tgss2  22907  ist1-2  23267  kgencn  23476  ptcnplem  23541  cnmptcom  23598  fbun  23760  cnflf  23922  fclsopn  23934  cnfcf  23962  isclmp  25030  isncvsngp  25082  caucfil  25216  ovolgelb  25414  dyadmax  25532  ftc1a  25977  ulmcau  26337  noetasuplem4  27681  conway  27745  cofcutr  27872  addsprop  27923  onsfi  28287  perpcom  28693  colinearalg  28890  uhgrvd00  29515  pthdlem2lem  29747  frgrwopregbsn  30296  phoeqi  30836  ho02i  31808  hoeq2  31810  adjsym  31812  cnvadj  31871  mddmd2  32288  cdj3lem3b  32419  mgccnv  32971  cvmlift2lem12  35294  elpotr  35762  fvineqsnf1  37391  poimirlem29  37636  heicant  37642  ispsubsp2  39733  fsuppind  42571  nla0003  43407  ntrclsiso  44049  ntrneiiso  44073  ntrneik2  44074  ntrneix2  44075  ntrneik3  44078  ntrneix3  44079  ntrneik13  44080  ntrneix13  44081  ntrneik4w  44082  imo72b2  44154  tratrb  44519  hbra2VD  44842  tratrbVD  44843  termopropd  49226