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 1819	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
3		alcom 2158	. . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
5		r2al 3182	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3182	. 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537   ∈ wcel 2107  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-11 2156

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-ral 3051

This theorem is referenced by:  rexcom  3275  ralrot3  3278  ralcom13  3279  ralcom13OLD  3280  2reu4lem  4504  ssint  4946  iinrab2  5052  disjxun  5123  reusv3  5387  cnvpo  6289  cnvso  6290  dfpo2  6298  fununi  6622  isocnv2  7334  dfsmo2  8370  tz7.48lem  8464  ixpiin  8947  boxriin  8963  dedekind  11407  rexfiuz  15369  gcdcllem1  16519  mreacs  17677  comfeq  17725  catpropd  17728  isnsg2  19148  cntzrec  19328  oppgsubm  19354  opprirred  20395  opprsubrng  20532  opprsubrg  20566  opprdomnb  20690  rmodislmodlem  20900  rmodislmod  20901  islindf4  21825  cpmatmcllem  22691  tgss2  22960  ist1-2  23320  kgencn  23529  ptcnplem  23594  cnmptcom  23651  fbun  23813  cnflf  23975  fclsopn  23987  cnfcf  24015  isclmp  25085  isncvsngp  25138  caucfil  25272  ovolgelb  25470  dyadmax  25588  ftc1a  26033  ulmcau  26393  noetasuplem4  27736  conway  27799  cofcutr  27913  addsprop  27964  perpcom  28676  colinearalg  28874  uhgrvd00  29499  pthdlem2lem  29734  frgrwopregbsn  30283  phoeqi  30823  ho02i  31795  hoeq2  31797  adjsym  31799  cnvadj  31858  mddmd2  32275  cdj3lem3b  32406  mgccnv  32935  cvmlift2lem12  35260  elpotr  35723  fvineqsnf1  37352  poimirlem29  37597  heicant  37603  ispsubsp2  39689  fsuppind  42545  nla0003  43383  ntrclsiso  44025  ntrneiiso  44049  ntrneik2  44050  ntrneix2  44051  ntrneik3  44054  ntrneix3  44055  ntrneik13  44056  ntrneix13  44057  ntrneik4w  44058  imo72b2  44130  tratrb  44501  hbra2VD  44825  tratrbVD  44826