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

Theorem rexcom 3277
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 3276 . . 3 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 ¬ 𝜑)
2 ralnex2 3122 . . 3 (∀𝑥𝐴𝑦𝐵 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴𝑦𝐵 𝜑)
3 ralnex2 3122 . . 3 (∀𝑦𝐵𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑦𝐵𝑥𝐴 𝜑)
41, 2, 33bitr3i 300 . 2 (¬ ∃𝑥𝐴𝑦𝐵 𝜑 ↔ ¬ ∃𝑦𝐵𝑥𝐴 𝜑)
54con4bii 320 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wral 3050  wrex 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-11 2146
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-ral 3051  df-rex 3060
This theorem is referenced by:  rexcom13  3283  2reurex  3752  2reu1  3887  2reu4lem  4527  iuncom  5004  xpiundi  5748  brdom7disj  10556  addcompr  11046  mulcompr  11048  qmulz  12968  elpq  12992  caubnd2  15340  ello1mpt2  15502  o1lo1  15517  lo1add  15607  lo1mul  15608  rlimno1  15636  sqrt2irr  16229  bezoutlem2  16519  bezoutlem4  16521  pythagtriplem19  16805  lsmcom2  19622  efgrelexlemb  19717  lsmcomx  19823  pgpfac1lem2  20044  pgpfac1lem4  20047  regsep2  23324  ordthaus  23332  tgcmp  23349  txcmplem1  23589  xkococnlem  23607  regr1lem2  23688  dyadmax  25571  coeeu  26204  ostth  27617  mulscom  28089  znegscl  28289  axpasch  28824  axeuclidlem  28845  usgr2pth0  29651  elwwlks2  29849  elwspths2spth  29850  shscom  31201  mdsymlem4  32288  mdsymlem8  32292  ordtconnlem1  33656  cvmliftlem15  35039  fvineqsneq  37022  lshpsmreu  38711  islpln5  39138  islvol5  39182  paddcom  39416  mapdrvallem2  41248  hdmapglem7a  41530  remexz  41707  hashnexinjle  41732  fsuppind  41958  fourierdlem42  45675  2rexsb  46619  2rexrsb  46620  pgrpgt2nabl  47616  islindeps2  47737  isldepslvec2  47739
  Copyright terms: Public domain W3C validator