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 3306
Description: Restricted quantifier version of 19.42v 1954 (see also 19.42 2237). (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 3303 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 464 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3213 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 464 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 306 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wrex 3110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3115
This theorem is referenced by:  rexcom  3311  ceqsrexbv  3601  ceqsrex2v  3602  2reuswap  3688  2reuswap2  3689  2reu5  3700  2rmoswap  3703  iunrab  4942  iunin2  4959  iundif2  4962  reusv2lem4  5270  iunopab  5414  cnvuni  5725  elidinxp  5882  xpdifid  5996  elunirn  6992  f1oiso  7087  oprabrexex2  7665  oeeu  8216  trcl  9158  dfac5lem2  9539  axgroth4  10247  rexuz2  12291  4fvwrd4  13026  cshwsexa  14181  divalglem10  15747  divalgb  15749  lsmelval2  19854  tgcmp  22010  hauscmplem  22015  unisngl  22136  xkobval  22195  txtube  22249  txcmplem1  22250  txkgen  22261  xkococnlem  22268  mbfaddlem  24268  mbfsup  24272  elaa  24916  dchrisumlem3  26079  colperpexlem3  26530  midex  26535  iscgra1  26608  ax5seg  26736  edglnl  26940  usgr2pth0  27558  hhcmpl  28987  sumdmdii  30202  reuxfrdf  30266  unipreima  30409  fpwrelmapffslem  30498  esumfsup  31443  reprdifc  32012  bnj168  32114  bnj1398  32420  cvmliftlem15  32659  dfpo2  33105  ellines  33727  bj-elsngl  34405  bj-dfmpoa  34534  ptrecube  35056  cnambfre  35104  islshpat  36312  lfl1dim  36416  glbconxN  36673  3dim0  36752  2dim  36765  1dimN  36766  islpln5  36830  islvol5  36874  dalem20  36988  lhpex2leN  37308  mapdval4N  38927  rexrabdioph  39728  rmxdioph  39950  expdiophlem1  39955  imaiun1  40345  coiun1  40346  ismnuprim  40995  prmunb2  41008  fourierdlem48  42789  2reuimp0  43663  2reuimp  43664  wtgoldbnnsum4prm  44313  bgoldbnnsum3prm  44315  islindeps2  44885  isldepslvec2  44887
  Copyright terms: Public domain W3C validator