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

Theorem r19.42v 3285
Description: Restricted quantifier version of 19.42v 1912 (see also 19.42 2169). (Contributed by NM, 27-May-1998.)
Assertion
Ref Expression
r19.42v (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.42v
StepHypRef Expression
1 r19.41v 3282 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 453 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3188 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 453 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 295 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 387  wrex 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-rex 3088
This theorem is referenced by:  rexcom  3290  ceqsrexbv  3558  ceqsrex2v  3559  2reuswap  3643  2reuswap2  3644  2reu5  3652  2rmoswap  3655  iunrab  4838  iunin2  4855  iundif2  4858  reusv2lem4  5151  iunopab  5294  cnvuni  5603  elidinxp  5753  xpdifid  5862  elunirn  6833  f1oiso  6925  oprabrexex2  7489  oeeu  8028  trcl  8962  dfac5lem2  9342  axgroth4  10050  rexuz2  12111  4fvwrd4  12841  cshwsexa  14046  divalglem10  15611  divalgb  15613  lsmelval2  19591  tgcmp  21725  hauscmplem  21730  unisngl  21851  xkobval  21910  txtube  21964  txcmplem1  21965  txkgen  21976  xkococnlem  21983  mbfaddlem  23976  mbfsup  23980  elaa  24620  dchrisumlem3  25781  colperpexlem3  26232  midex  26237  iscgra1  26310  ax5seg  26439  edglnl  26643  usgr2pth0  27266  hhcmpl  28768  sumdmdii  29985  unipreima  30167  fpwrelmapffslem  30241  esumfsup  31002  reprdifc  31575  bnj168  31677  bnj1398  31980  cvmliftlem15  32159  dfpo2  32540  ellines  33163  bj-elsngl  33827  bj-dfmpoa  33948  ptrecube  34362  cnambfre  34410  islshpat  35627  lfl1dim  35731  glbconxN  35988  3dim0  36067  2dim  36080  1dimN  36081  islpln5  36145  islvol5  36189  dalem20  36303  lhpex2leN  36623  mapdval4N  38242  rexrabdioph  38816  rmxdioph  39038  expdiophlem1  39043  imaiun1  39388  coiun1  39389  ismnuprim  40034  prmunb2  40088  fourierdlem48  41895  2reuimp0  42744  2reuimp  42745  wtgoldbnnsum4prm  43360  bgoldbnnsum3prm  43362  islindeps2  43930  isldepslvec2  43932
  Copyright terms: Public domain W3C validator