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

Theorem rexcom 3290
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 3289 . . 3 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 ¬ 𝜑)
2 ralnex2 3133 . . 3 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
3 ralnex2 3133 . . 3 (∀𝑦𝐵𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦𝐵𝑥𝐴 𝜑)
41, 2, 33bitr3i 301 . 2 (¬ ∃𝑥𝐴𝑦𝐵 𝜑 ↔ ¬ ∃𝑦𝐵𝑥𝐴 𝜑)
54con4bii 321 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wral 3061  wrex 3070
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 2157
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071
This theorem is referenced by:  rexcom13  3296  2reurex  3766  2reu1  3897  2reu4lem  4522  iuncom  4999  xpiundi  5756  brdom7disj  10571  addcompr  11061  mulcompr  11063  qmulz  12993  elpq  13017  caubnd2  15396  ello1mpt2  15558  o1lo1  15573  lo1add  15663  lo1mul  15664  rlimno1  15690  sqrt2irr  16285  bezoutlem2  16577  bezoutlem4  16579  pythagtriplem19  16871  lsmcom2  19673  efgrelexlemb  19768  lsmcomx  19874  pgpfac1lem2  20095  pgpfac1lem4  20098  regsep2  23384  ordthaus  23392  tgcmp  23409  txcmplem1  23649  xkococnlem  23667  regr1lem2  23748  dyadmax  25633  coeeu  26264  ostth  27683  mulscom  28165  znegscl  28378  axpasch  28956  axeuclidlem  28977  usgr2pth0  29785  elwwlks2  29986  elwspths2spth  29987  shscom  31338  mdsymlem4  32425  mdsymlem8  32429  ordtconnlem1  33923  cvmliftlem15  35303  fvineqsneq  37413  lshpsmreu  39110  islpln5  39537  islvol5  39581  paddcom  39815  mapdrvallem2  41647  hdmapglem7a  41929  remexz  42105  hashnexinjle  42130  fimgmcyclem  42543  fsuppind  42600  fourierdlem42  46164  2rexsb  47113  2rexrsb  47114  pgrpgt2nabl  48282  islindeps2  48400  isldepslvec2  48402
  Copyright terms: Public domain W3C validator