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

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

Proof of Theorem rexcom
StepHypRef Expression
1 nfcv 2761 . 2 𝑦𝐴
2 nfcv 2761 . 2 𝑥𝐵
31, 2rexcomf 3091 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914
This theorem is referenced by:  rexcom13  3095  rexcom4  3215  iuncom  4500  xpiundi  5144  brdom7disj  9313  addcompr  9803  mulcompr  9805  qmulz  11751  caubnd2  14047  ello1mpt2  14203  o1lo1  14218  lo1add  14307  lo1mul  14308  rlimno1  14334  sqrt2irr  14922  bezoutlem2  15200  bezoutlem4  15202  pythagtriplem19  15481  lsmcom2  18010  efgrelexlemb  18103  lsmcomx  18199  pgpfac1lem2  18414  pgpfac1lem4  18417  regsep2  21120  ordthaus  21128  tgcmp  21144  txcmplem1  21384  xkococnlem  21402  regr1lem2  21483  dyadmax  23306  coeeu  23919  ostth  25262  axpasch  25755  axeuclidlem  25776  usgr2pth0  26564  elwwlks2  26762  elwspths2spth  26763  frgrwopreglem5  27077  shscom  28066  mdsymlem4  29153  mdsymlem8  29157  ordtconnlem1  29794  cvmliftlem15  31041  lshpsmreu  33915  islpln5  34340  islvol5  34384  paddcom  34618  mapdrvallem2  36453  hdmapglem7a  36738  fourierdlem42  39703  2rexsb  40504  2rexrsb  40505  2reurex  40515  2reu1  40520  2reu4a  40523  pgrpgt2nabl  41465  islindeps2  41590  isldepslvec2  41592
  Copyright terms: Public domain W3C validator