Theorem ralcom 3262

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2113  ∀wral 3049

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 2162

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050

This theorem is referenced by:  rexcom  3263  ralrot3  3265  ralcom13  3266  2reu4lem  4474  ssint  4917  iinrab2  5023  disjxun  5094  reusv3  5348  cnvpo  6243  cnvso  6244  dfpo2  6252  fununi  6565  isocnv2  7275  dfsmo2  8277  tz7.48lem  8370  ixpiin  8860  boxriin  8876  dedekind  11294  rexfiuz  15269  gcdcllem1  16424  mreacs  17579  comfeq  17627  catpropd  17630  isnsg2  19083  cntzrec  19263  oppgsubm  19289  opprirred  20356  opprsubrng  20490  opprsubrg  20524  opprdomnb  20648  rmodislmodlem  20878  rmodislmod  20879  islindf4  21791  cpmatmcllem  22660  tgss2  22929  ist1-2  23289  kgencn  23498  ptcnplem  23563  cnmptcom  23620  fbun  23782  cnflf  23944  fclsopn  23956  cnfcf  23984  isclmp  25051  isncvsngp  25103  caucfil  25237  ovolgelb  25435  dyadmax  25553  ftc1a  25998  ulmcau  26358  noetasuplem4  27702  conway  27767  cofcutr  27895  addsprop  27946  onsfi  28316  perpcom  28734  colinearalg  28932  uhgrvd00  29557  pthdlem2lem  29789  frgrwopregbsn  30341  phoeqi  30881  ho02i  31853  hoeq2  31855  adjsym  31857  cnvadj  31916  mddmd2  32333  cdj3lem3b  32464  mgccnv  33030  cvmlift2lem12  35457  elpotr  35922  fvineqsnf1  37554  poimirlem29  37789  heicant  37795  ispsubsp2  39945  fsuppind  42775  nla0003  43608  ntrclsiso  44250  ntrneiiso  44274  ntrneik2  44275  ntrneix2  44276  ntrneik3  44279  ntrneix3  44280  ntrneik13  44281  ntrneix13  44282  ntrneik4w  44283  imo72b2  44355  tratrb  44719  hbra2VD  45042  tratrbVD  45043  termopropd  49431