Theorem ralcom 3274

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

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

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 3053

This theorem is referenced by:  rexcom  3275  ralrot3  3278  ralcom13  3279  ralcom13OLD  3280  2reu4lem  4502  ssint  4945  iinrab2  5051  disjxun  5122  reusv3  5380  cnvpo  6281  cnvso  6282  dfpo2  6290  fununi  6616  isocnv2  7329  dfsmo2  8366  tz7.48lem  8460  ixpiin  8943  boxriin  8959  dedekind  11403  rexfiuz  15371  gcdcllem1  16523  mreacs  17675  comfeq  17723  catpropd  17726  isnsg2  19144  cntzrec  19324  oppgsubm  19350  opprirred  20387  opprsubrng  20524  opprsubrg  20558  opprdomnb  20682  rmodislmodlem  20891  rmodislmod  20892  islindf4  21803  cpmatmcllem  22661  tgss2  22930  ist1-2  23290  kgencn  23499  ptcnplem  23564  cnmptcom  23621  fbun  23783  cnflf  23945  fclsopn  23957  cnfcf  23985  isclmp  25053  isncvsngp  25106  caucfil  25240  ovolgelb  25438  dyadmax  25556  ftc1a  26001  ulmcau  26361  noetasuplem4  27705  conway  27768  cofcutr  27889  addsprop  27940  onsfi  28304  perpcom  28697  colinearalg  28894  uhgrvd00  29519  pthdlem2lem  29754  frgrwopregbsn  30303  phoeqi  30843  ho02i  31815  hoeq2  31817  adjsym  31819  cnvadj  31878  mddmd2  32295  cdj3lem3b  32426  mgccnv  32984  cvmlift2lem12  35341  elpotr  35804  fvineqsnf1  37433  poimirlem29  37678  heicant  37684  ispsubsp2  39770  fsuppind  42588  nla0003  43424  ntrclsiso  44066  ntrneiiso  44090  ntrneik2  44091  ntrneix2  44092  ntrneik3  44095  ntrneix3  44096  ntrneik13  44097  ntrneix13  44098  ntrneik4w  44099  imo72b2  44171  tratrb  44536  hbra2VD  44859  tratrbVD  44860  termopropd  49141