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

Theorem r19.42v 3073
 Description: Restricted quantifier version of 19.42v 1905 (see also 19.42 2092). (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 3070 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 465 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3023 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 465 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 291 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902 This theorem is referenced by:  ceqsrexbv  3307  ceqsrex2v  3308  2reuswap  3377  2reu5  3383  rabasiun  4459  iunrab  4503  iunin2  4520  iundif2  4523  reusv2lem4  4798  iunopab  4936  elxp2OLD  5057  cnvuni  5231  xpdifid  5481  elunirn  6413  f1oiso  6501  oprabrexex2  7049  oeeu  7570  trcl  8487  dfac5lem2  8830  axgroth4  9533  rexuz2  11615  4fvwrd4  12328  cshwsexa  13421  divalglem10  14963  divalgb  14965  lsmelval2  18906  tgcmp  21014  hauscmplem  21019  unisngl  21140  xkobval  21199  txtube  21253  txcmplem1  21254  txkgen  21265  xkococnlem  21272  mbfaddlem  23233  mbfsup  23237  elaa  23875  dchrisumlem3  24980  colperpexlem3  25424  midex  25429  iscgra1  25502  ax5seg  25618  usg2spot2nb  26592  usgreg2spot  26594  sumdmdii  28658  2reuswap2  28712  unipreima  28826  fpwrelmapffslem  28895  esumfsup  29459  bnj168  30052  bnj1398  30356  cvmliftlem15  30534  dfpo2  30898  ellines  31429  bj-elsngl  32149  bj-dfmpt2a  32252  ptrecube  32579  cnambfre  32628  islshpat  33322  lfl1dim  33426  glbconxN  33682  3dim0  33761  2dim  33774  1dimN  33775  islpln5  33839  islvol5  33883  dalem20  33997  lhpex2leN  34317  mapdval4N  35939  rexrabdioph  36376  rmxdioph  36601  expdiophlem1  36606  imaiun1  36962  coiun1  36963  prmunb2  37532  fourierdlem48  39047  2rmoswap  39833  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  usgr2pth0  40971  fusgr2wsp2nb  41498  islindeps2  42066  isldepslvec2  42068
 Copyright terms: Public domain W3C validator