Theorem ralcom 3265

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045

This theorem is referenced by:  rexcom  3266  ralrot3  3268  ralcom13  3269  ralcom13OLD  3270  2reu4lem  4485  ssint  4928  iinrab2  5034  disjxun  5105  reusv3  5360  cnvpo  6260  cnvso  6261  dfpo2  6269  fununi  6591  isocnv2  7306  dfsmo2  8316  tz7.48lem  8409  ixpiin  8897  boxriin  8913  dedekind  11337  rexfiuz  15314  gcdcllem1  16469  mreacs  17619  comfeq  17667  catpropd  17670  isnsg2  19088  cntzrec  19268  oppgsubm  19294  opprirred  20331  opprsubrng  20468  opprsubrg  20502  opprdomnb  20626  rmodislmodlem  20835  rmodislmod  20836  islindf4  21747  cpmatmcllem  22605  tgss2  22874  ist1-2  23234  kgencn  23443  ptcnplem  23508  cnmptcom  23565  fbun  23727  cnflf  23889  fclsopn  23901  cnfcf  23929  isclmp  24997  isncvsngp  25049  caucfil  25183  ovolgelb  25381  dyadmax  25499  ftc1a  25944  ulmcau  26304  noetasuplem4  27648  conway  27711  cofcutr  27832  addsprop  27883  onsfi  28247  perpcom  28640  colinearalg  28837  uhgrvd00  29462  pthdlem2lem  29697  frgrwopregbsn  30246  phoeqi  30786  ho02i  31758  hoeq2  31760  adjsym  31762  cnvadj  31821  mddmd2  32238  cdj3lem3b  32369  mgccnv  32925  cvmlift2lem12  35301  elpotr  35769  fvineqsnf1  37398  poimirlem29  37643  heicant  37649  ispsubsp2  39740  fsuppind  42578  nla0003  43414  ntrclsiso  44056  ntrneiiso  44080  ntrneik2  44081  ntrneix2  44082  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  imo72b2  44161  tratrb  44526  hbra2VD  44849  tratrbVD  44850  termopropd  49233