Theorem ralcom 3284

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1531   ∈ wcel 2098  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-11 2146

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-ral 3059

This theorem is referenced by:  rexcom  3285  ralrot3  3288  ralcom13  3289  ralcom13OLD  3290  2reu4lem  4529  ssint  4971  iinrab2  5077  disjxun  5150  reusv3  5409  cnvpo  6296  cnvso  6297  dfpo2  6305  fununi  6633  isocnv2  7345  dfsmo2  8374  tz7.48lem  8468  ixpiin  8949  boxriin  8965  dedekind  11415  rexfiuz  15334  gcdcllem1  16481  mreacs  17645  comfeq  17693  catpropd  17696  isnsg2  19118  cntzrec  19294  oppgsubm  19323  opprirred  20368  opprsubrng  20503  opprsubrg  20539  rmodislmodlem  20819  rmodislmod  20820  rmodislmodOLD  20821  islindf4  21779  cpmatmcllem  22640  tgss2  22910  ist1-2  23271  kgencn  23480  ptcnplem  23545  cnmptcom  23602  fbun  23764  cnflf  23926  fclsopn  23938  cnfcf  23966  isclmp  25044  isncvsngp  25097  caucfil  25231  ovolgelb  25429  dyadmax  25547  ftc1a  25992  ulmcau  26351  noetasuplem4  27689  conway  27752  cofcutr  27864  addsprop  27913  perpcom  28537  colinearalg  28741  uhgrvd00  29368  pthdlem2lem  29601  frgrwopregbsn  30147  phoeqi  30687  ho02i  31659  hoeq2  31661  adjsym  31663  cnvadj  31722  mddmd2  32139  cdj3lem3b  32270  mgccnv  32747  cvmlift2lem12  34957  elpotr  35410  fvineqsnf1  36922  poimirlem29  37155  heicant  37161  ispsubsp2  39251  fsuppind  41854  nla0003  42886  ntrclsiso  43528  ntrneiiso  43552  ntrneik2  43553  ntrneix2  43554  ntrneik3  43557  ntrneix3  43558  ntrneik13  43559  ntrneix13  43560  ntrneik4w  43561  imo72b2  43633  tratrb  44006  hbra2VD  44330  tratrbVD  44331