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

Theorem rexcom 3272
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.) (Proof shortened by Wolf Lammen, 8-Dec-2024.)
Assertion
Ref Expression
rexcom (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem rexcom
StepHypRef Expression
1 ralcom 3271 . . 3 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 ¬ 𝜑)
2 ralnex2 3127 . . 3 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
3 ralnex2 3127 . . 3 (∀𝑦𝐵𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦𝐵𝑥𝐴 𝜑)
41, 2, 33bitr3i 301 . 2 (¬ ∃𝑥𝐴𝑦𝐵 𝜑 ↔ ¬ ∃𝑦𝐵𝑥𝐴 𝜑)
54con4bii 321 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-11 2155
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3062  df-rex 3071
This theorem is referenced by:  rexcom13  3278  2reurex  3719  2reu1  3854  2reu4lem  4484  iuncom  4962  xpiundi  5703  brdom7disj  10472  addcompr  10962  mulcompr  10964  qmulz  12881  elpq  12905  caubnd2  15248  ello1mpt2  15410  o1lo1  15425  lo1add  15515  lo1mul  15516  rlimno1  15544  sqrt2irr  16136  bezoutlem2  16426  bezoutlem4  16428  pythagtriplem19  16710  lsmcom2  19442  efgrelexlemb  19537  lsmcomx  19639  pgpfac1lem2  19859  pgpfac1lem4  19862  regsep2  22743  ordthaus  22751  tgcmp  22768  txcmplem1  23008  xkococnlem  23026  regr1lem2  23107  dyadmax  24978  coeeu  25602  ostth  27003  axpasch  27932  axeuclidlem  27953  usgr2pth0  28755  elwwlks2  28953  elwspths2spth  28954  shscom  30303  mdsymlem4  31390  mdsymlem8  31394  ordtconnlem1  32562  cvmliftlem15  33949  fvineqsneq  35929  lshpsmreu  37617  islpln5  38044  islvol5  38088  paddcom  38322  mapdrvallem2  40154  hdmapglem7a  40436  fsuppind  40808  fourierdlem42  44476  2rexsb  45419  2rexrsb  45420  pgrpgt2nabl  46528  islindeps2  46650  isldepslvec2  46652
  Copyright terms: Public domain W3C validator