Theorem ralcom 3299

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-11 2198

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086

This theorem is referenced by:  rexcom  3300  ralrot3  3302  ralcom13  3303  2reu4lem  4489  ssint  4933  iinrab2  5038  disjxun  5111  reusv3  5377  cnvpo  6289  cnvso  6290  dfpo2  6298  fununi  6612  isocnv2  7330  dfsmo2  8334  tz7.48lem  8428  ixpiin  8922  boxriin  8938  dedekind  11373  rexfiuz  15399  gcdcllem1  16557  mreacs  17714  comfeq  17762  catpropd  17765  isnsg2  19222  cntzrec  19406  oppgsubm  19432  opprirred  20504  opprsubrng  20644  opprsubrg  20678  opprdomnb  20801  rmodislmodlem  21028  rmodislmod  21029  islindf4  21957  cpmatmcllem  22844  tgss2  23113  ist1-2  23473  kgencn  23682  ptcnplem  23747  cnmptcom  23804  fbun  23966  cnflf  24128  fclsopn  24140  cnfcf  24168  isclmp  25225  isncvsngp  25277  caucfil  25411  ovolgelb  25608  dyadmax  25726  ftc1a  26165  ulmcau  26524  noetasuplem4  27866  conway  27938  cofcutr  28083  addsprop  28135  onsfi  28515  perpcom  28952  colinearalg  29201  uhgrvd00  29825  pthdlem2lem  30057  frgrwopregbsn  30609  phoeqi  31150  ho02i  32122  hoeq2  32124  adjsym  32126  cnvadj  32185  mddmd2  32602  cdj3lem3b  32733  mgccnv  33260  cvmlift2lem12  35705  elpotr  36170  nmulcom  36585  fvineqsnf1  37944  poimirlem29  38188  heicant  38194  disjimeceqim  39343  ispsubsp2  40410  fsuppind  43214  nla0003  44043  ntrclsiso  44685  ntrneiiso  44709  ntrneik2  44710  ntrneix2  44711  ntrneik3  44714  ntrneix3  44715  ntrneik13  44716  ntrneix13  44717  ntrneik4w  44718  imo72b2  44790  tratrb  45137  hbra2VD  45460  tratrbVD  45461  termopropd  49907