Theorem ralcom 3293

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   ∈ wcel 2146  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-11 2196

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3080

This theorem is used by:  rexcom  3294  ralrot3  3296  ralcom13  3297  2reu4lem  4481  ssint  4926  iinrab2  5030  disjxun  5103  reusv3  5370  cnvpo  6296  cnvso  6297  dfpo2  6305  fununi  6623  isocnv2  7346  dfsmo2  8366  tz7.48lemOLD  8462  ixpiin  8963  boxriin  8979  dedekind  11483  rexfiuz  15527  gcdcllem1  16681  mreacs  17844  comfeq  17892  catpropd  17895  isnsg2  19378  cntzrec  19562  oppgsubm  19588  opprirred  20664  opprsubrng  20823  opprsubrg  20857  opprdomnb  20980  rmodislmodlem  21216  rmodislmod  21217  islindf4  22156  cpmatmcllem  23048  tgss2  23317  ist1-2  23677  kgencn  23887  ptcnplem  23952  cnmptcom  24009  fbun  24171  cnflf  24333  fclsopn  24345  cnfcf  24373  isclmp  25430  isncvsngp  25482  caucfil  25616  ovolgelb  25813  dyadmax  25931  ftc1a  26369  ulmcau  26734  noetasuplem4  28105  conway  28177  cofcutr  28322  addsprop  28374  onsfi  28754  perpcom  29200  colinearalg  29500  uhgrvd00  30127  pthdlem2lem  30365  frgrwopregbsn  30930  phoeqi  31471  ho02i  32443  hoeq2  32445  adjsym  32447  cnvadj  32506  mddmd2  32923  cdj3lem3b  33054  mgccnv  33613  cvmlift2lem12  36200  elpotr  36670  nmulcom  37070  fvineqsnf1  38473  poimirlem29  38707  heicant  38713  disjimeceqim  39876  ispsubsp2  40943  fsuppind  43758  nla0003  44566  ntrclsiso  45207  ntrneiiso  45231  ntrneik2  45232  ntrneix2  45233  ntrneik3  45236  ntrneix3  45237  ntrneik13  45238  ntrneix13  45239  ntrneik4w  45240  imo72b2  45312  tratrb  45658  hbra2VD  45981  tratrbVD  45982  termopropd  50505