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 3069
Description: Restricted quantifier version of 19.42v 1904 (see also 19.42 2090). (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 3066 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 464 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3019 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 464 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 290 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wrex 2893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-rex 2898
This theorem is referenced by:  ceqsrexbv  3303  ceqsrex2v  3304  2reuswap  3373  2reu5  3379  rabasiun  4450  iunrab  4494  iunin2  4511  iundif2  4514  reusv2lem4  4790  iunopab  4923  elxp2OLD  5044  cnvuni  5216  xpdifid  5464  elunirn  6388  f1oiso  6476  oprabrexex2  7023  oeeu  7544  trcl  8461  dfac5lem2  8804  axgroth4  9507  rexuz2  11568  4fvwrd4  12280  cshwsexa  13364  divalglem10  14906  divalgb  14908  lsmelval2  18849  tgcmp  20953  hauscmplem  20958  unisngl  21079  xkobval  21138  txtube  21192  txcmplem1  21193  txkgen  21204  xkococnlem  21211  mbfaddlem  23147  mbfsup  23151  elaa  23789  dchrisumlem3  24894  colperpexlem3  25339  midex  25344  iscgra1  25417  ax5seg  25533  usg2spot2nb  26355  usgreg2spot  26357  sumdmdii  28461  2reuswap2  28515  unipreima  28629  fpwrelmapffslem  28698  esumfsup  29262  bnj168  29855  bnj1398  30159  cvmliftlem15  30337  dfpo2  30701  ellines  31232  bj-elsngl  31949  bj-dfmpt2a  32052  ptrecube  32379  cnambfre  32428  islshpat  33122  lfl1dim  33226  glbconxN  33482  3dim0  33561  2dim  33574  1dimN  33575  islpln5  33639  islvol5  33683  dalem20  33797  lhpex2leN  34117  mapdval4N  35739  rexrabdioph  36176  rmxdioph  36401  expdiophlem1  36406  imaiun1  36762  coiun1  36763  prmunb2  37332  fourierdlem48  38848  2rmoswap  39634  wtgoldbnnsum4prm  40020  bgoldbnnsum3prm  40022  usgr2pth0  40970  fusgr2wsp2nb  41497  islindeps2  42065  isldepslvec2  42067
  Copyright terms: Public domain W3C validator