Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexcom Structured version   Visualization version   GIF version

Theorem rexcom 3353
 Description: Commutation of restricted existential quantifiers. (Contributed by NM, 19-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) (Proof shortened by BJ, 26-Aug-2023.)
Assertion
Ref Expression
rexcom (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐵   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem rexcom
StepHypRef Expression
1 df-rex 3142 . . 3 (∃𝑦𝐵 𝜑 ↔ ∃𝑦(𝑦𝐵𝜑))
21rexbii 3245 . 2 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦(𝑦𝐵𝜑))
3 rexcom4 3247 . 2 (∃𝑥𝐴𝑦(𝑦𝐵𝜑) ↔ ∃𝑦𝑥𝐴 (𝑦𝐵𝜑))
4 r19.42v 3348 . . . 4 (∃𝑥𝐴 (𝑦𝐵𝜑) ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
54exbii 1842 . . 3 (∃𝑦𝑥𝐴 (𝑦𝐵𝜑) ↔ ∃𝑦(𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
6 df-rex 3142 . . 3 (∃𝑦𝐵𝑥𝐴 𝜑 ↔ ∃𝑦(𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
75, 6bitr4i 280 . 2 (∃𝑦𝑥𝐴 (𝑦𝐵𝜑) ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
82, 3, 73bitri 299 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1774   ∈ wcel 2108  ∃wrex 3137 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-11 2154 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-rex 3142 This theorem is referenced by:  rexcom13  3358  rexcom4OLD  3525  2reurex  3748  2reu1  3879  2reu4lem  4463  iuncom  4917  xpiundi  5615  brdom7disj  9945  addcompr  10435  mulcompr  10437  qmulz  12343  elpq  12366  caubnd2  14709  ello1mpt2  14871  o1lo1  14886  lo1add  14975  lo1mul  14976  rlimno1  15002  sqrt2irr  15594  bezoutlem2  15880  bezoutlem4  15882  pythagtriplem19  16162  lsmcom2  18772  efgrelexlemb  18868  lsmcomx  18968  pgpfac1lem2  19189  pgpfac1lem4  19192  regsep2  21976  ordthaus  21984  tgcmp  22001  txcmplem1  22241  xkococnlem  22259  regr1lem2  22340  dyadmax  24191  coeeu  24807  ostth  26207  axpasch  26719  axeuclidlem  26740  usgr2pth0  27538  elwwlks2  27737  elwspths2spth  27738  shscom  29088  mdsymlem4  30175  mdsymlem8  30179  ordtconnlem1  31160  cvmliftlem15  32538  fvineqsneq  34685  lshpsmreu  36237  islpln5  36663  islvol5  36707  paddcom  36941  mapdrvallem2  38773  hdmapglem7a  39055  fourierdlem42  42425  2rexsb  43290  2rexrsb  43291  pgrpgt2nabl  44405  islindeps2  44529  isldepslvec2  44531
 Copyright terms: Public domain W3C validator