Theorem ralcom 3280

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-11 2156

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068

This theorem is referenced by:  ralcom13  3284  ralrot3  3286  2reu4lem  4453  ssint  4892  iinrab2  4995  disjxun  5068  reusv3  5323  cnvpo  6179  cnvso  6180  dfpo2  6188  fununi  6493  isocnv2  7182  dfsmo2  8149  tz7.48lem  8242  ixpiin  8670  boxriin  8686  dedekind  11068  rexfiuz  14987  gcdcllem1  16134  mreacs  17284  comfeq  17332  catpropd  17335  isnsg2  18699  cntzrec  18855  oppgsubm  18884  opprirred  19859  opprsubrg  19960  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  islindf4  20955  cpmatmcllem  21775  tgss2  22045  ist1-2  22406  kgencn  22615  ptcnplem  22680  cnmptcom  22737  fbun  22899  cnflf  23061  fclsopn  23073  cnfcf  23101  isclmp  24166  isncvsngp  24218  caucfil  24352  ovolgelb  24549  dyadmax  24667  ftc1a  25106  ulmcau  25459  perpcom  26978  colinearalg  27181  uhgrvd00  27804  pthdlem2lem  28036  frgrwopregbsn  28582  phoeqi  29120  ho02i  30092  hoeq2  30094  adjsym  30096  cnvadj  30155  mddmd2  30572  cdj3lem3b  30703  mgccnv  31179  cvmlift2lem12  33176  elpotr  33663  noetasuplem4  33866  conway  33920  cofcutr  34019  fvineqsnf1  35508  poimirlem29  35733  heicant  35739  ispsubsp2  37687  fsuppind  40202  ntrclsiso  41566  ntrneiiso  41590  ntrneik2  41591  ntrneix2  41592  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  ntrneik4w  41599  imo72b2  41672  tratrb  42045  hbra2VD  42369  tratrbVD  42370