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 3239
Description: Restricted quantifier version of 19.42v 2048 (see also 19.42 2270). (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 3236 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 452 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3188 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 452 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 294 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-rex 3061
This theorem is referenced by:  ceqsrexbv  3490  ceqsrex2v  3491  2reuswap  3571  2reu5  3577  iunrab  4723  iunin2  4740  iundif2  4743  reusv2lem4  5036  iunopab  5173  cnvuni  5477  elidinxp  5632  xpdifid  5745  elunirn  6701  f1oiso  6793  oprabrexex2  7356  oeeu  7888  trcl  8819  dfac5lem2  9198  axgroth4  9907  rexuz2  11939  4fvwrd4  12667  cshwsexa  13855  divalglem10  15409  divalgb  15411  lsmelval2  19357  tgcmp  21484  hauscmplem  21489  unisngl  21610  xkobval  21669  txtube  21723  txcmplem1  21724  txkgen  21735  xkococnlem  21742  mbfaddlem  23718  mbfsup  23722  elaa  24362  dchrisumlem3  25471  colperpexlem3  25915  midex  25920  iscgra1  25993  ax5seg  26109  edglnl  26316  usgr2pth0  26952  hhcmpl  28448  sumdmdii  29665  2reuswap2  29717  unipreima  29831  fpwrelmapffslem  29891  esumfsup  30514  reprdifc  31088  bnj168  31179  bnj1398  31482  cvmliftlem15  31660  dfpo2  32022  ellines  32635  bj-elsngl  33315  bj-dfmpt2a  33431  ptrecube  33765  cnambfre  33813  islshpat  34905  lfl1dim  35009  glbconxN  35266  3dim0  35345  2dim  35358  1dimN  35359  islpln5  35423  islvol5  35467  dalem20  35581  lhpex2leN  35901  mapdval4N  37520  rexrabdioph  37968  rmxdioph  38192  expdiophlem1  38197  imaiun1  38550  coiun1  38551  prmunb2  39116  fourierdlem48  40940  2rmoswap  41787  wtgoldbnnsum4prm  42298  bgoldbnnsum3prm  42300  islindeps2  42873  isldepslvec2  42875
  Copyright terms: Public domain W3C validator