Theorem ralcom 3354

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2161

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3143

This theorem is referenced by:  ralcom13  3359  ralrot3  3361  ralcom4OLD  3525  2reu4lem  4465  ssint  4892  iinrab2  4992  disjxun  5064  reusv3  5306  cnvpo  6138  cnvso  6139  fununi  6429  isocnv2  7084  dfsmo2  7984  tz7.48lem  8077  ixpiin  8488  boxriin  8504  dedekind  10803  rexfiuz  14707  gcdcllem1  15848  mreacs  16929  comfeq  16976  catpropd  16979  isnsg2  18308  cntzrec  18464  oppgsubm  18490  opprirred  19452  opprsubrg  19556  rmodislmodlem  19701  rmodislmod  19702  islindf4  20982  cpmatmcllem  21326  tgss2  21595  ist1-2  21955  kgencn  22164  ptcnplem  22229  cnmptcom  22286  fbun  22448  cnflf  22610  fclsopn  22622  cnfcf  22650  isclmp  23701  isncvsngp  23753  caucfil  23886  ovolgelb  24081  dyadmax  24199  ftc1a  24634  ulmcau  24983  perpcom  26499  colinearalg  26696  uhgrvd00  27316  pthdlem2lem  27548  frgrwopregbsn  28096  phoeqi  28634  ho02i  29606  hoeq2  29608  adjsym  29610  cnvadj  29669  mddmd2  30086  cdj3lem3b  30217  cvmlift2lem12  32561  dfpo2  32991  elpotr  33026  noetalem3  33219  conway  33264  fvineqsnf1  34694  poimirlem29  34936  heicant  34942  ispsubsp2  36897  ntrclsiso  40466  ntrneiiso  40490  ntrneik2  40491  ntrneix2  40492  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  ntrneik4w  40499  imo72b2  40574  tratrb  40919  hbra2VD  41243  tratrbVD  41244