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

Theorem rexcom4 3216
Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
rexcom4 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rexcom4
StepHypRef Expression
1 rexcom 3096 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥𝐴 𝜑)
2 rexv 3211 . . 3 (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
32rexbii 3039 . 2 (∃𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∃𝑥𝐴𝑦𝜑)
4 rexv 3211 . 2 (∃𝑦 ∈ V ∃𝑥𝐴 𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 290 1 (∃𝑥𝐴𝑦𝜑 ↔ ∃𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1701  wrex 2913  Vcvv 3191
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 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
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 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-v 3193
This theorem is referenced by:  rexcom4a  3217  reuind  3398  uni0b  4434  iuncom4  4499  dfiun2g  4523  iunn0  4551  iunxiun  4579  iinexg  4789  inuni  4791  iunopab  4977  xpiundi  5139  xpiundir  5140  cnvuni  5274  dmiun  5298  elres  5398  elsnres  5399  rniun  5506  xpdifid  5525  imaco  5602  coiun  5607  abrexco  6457  imaiun  6458  fliftf  6520  fun11iun  7076  oprabrexex2  7106  releldm2  7166  oarec  7588  omeu  7611  eroveu  7788  dfac5lem2  8892  genpass  9776  supaddc  10935  supadd  10936  supmul1  10937  supmullem2  10939  supmul  10940  pceu  15470  4sqlem12  15579  mreiincl  16172  psgneu  17842  ntreq0  20786  unisngl  21235  metrest  22234  metuel2  22275  istrkg2ld  25254  fpwrelmapffslem  29341  omssubaddlem  30134  omssubadd  30135  bnj906  30700  nosino  31567  nosifv  31568  bj-elsngl  32595  bj-restn0  32672  ismblfin  33068  itg2addnclem3  33081  sdclem1  33157  prter2  33632  lshpsmreu  33862  islpln5  34287  islvol5  34331  cdlemftr3  35319  mapdpglem3  36430  hdmapglem7a  36685  diophrex  36805  imaiun1  37410  coiun1  37411  upbdrech  38970
  Copyright terms: Public domain W3C validator