Theorem ralcom 3294

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-11 2197

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081

This theorem is used by:  rexcom  3295  ralrot3  3297  ralcom13  3298  2reu4lem  4482  ssint  4929  iinrab2  5033  disjxun  5106  reusv3  5374  cnvpo  6314  cnvso  6315  dfpo2  6325  fununi  6645  isocnv2  7370  dfsmo2  8393  tz7.48lemOLD  8489  ixpiin  8990  boxriin  9006  dedekind  11512  rexfiuz  15559  gcdcllem1  16713  mreacs  17882  comfeq  17930  catpropd  17933  isnsg2  19416  cntzrec  19601  oppgsubm  19627  opprirred  20703  opprsubrng  20862  opprsubrg  20896  opprdomnb  21019  rmodislmodlem  21255  rmodislmod  21256  islindf4  22199  cpmatmcllem  23091  tgss2  23360  ist1-2  23720  kgencn  23930  ptcnplem  23995  cnmptcom  24052  fbun  24214  cnflf  24376  fclsopn  24388  cnfcf  24416  isclmp  25473  isncvsngp  25525  caucfil  25659  ovolgelb  25856  dyadmax  25974  ftc1a  26412  ulmcau  26779  noetasuplem4  28150  conway  28222  cofcutr  28367  addsprop  28419  onsfi  28799  perpcom  29245  colinearalg  29545  uhgrvd00  30172  pthdlem2lem  30410  frgrwopregbsn  30975  phoeqi  31516  ho02i  32488  hoeq2  32490  adjsym  32492  cnvadj  32551  mddmd2  32968  cdj3lem3b  33099  mgccnv  33659  cvmlift2lem12  36287  elpotr  36758  nmulcom  37158  fvineqsnf1  38601  poimirlem29  38835  heicant  38841  disjimeceqim  40002  ispsubsp2  41069  fsuppind  43884  nla0003  44687  ntrclsiso  45328  ntrneiiso  45352  ntrneik2  45353  ntrneix2  45354  ntrneik3  45357  ntrneix3  45358  ntrneik13  45359  ntrneix13  45360  ntrneik4w  45361  imo72b2  45433  tratrb  45779  hbra2VD  46102  tratrbVD  46103  termopropd  50697