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 3230
Description: Restricted quantifier version of 19.42v 2030 (see also 19.42 2252). (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 3227 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 465 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3179 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 465 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 292 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-rex 3056
This theorem is referenced by:  ceqsrexbv  3476  ceqsrex2v  3477  2reuswap  3551  2reu5  3557  iunrab  4719  iunin2  4736  iundif2  4739  reusv2lem4  5021  iunopab  5162  elxp2OLD  5290  cnvuni  5464  xpdifid  5720  elunirn  6672  f1oiso  6764  oprabrexex2  7323  oeeu  7852  trcl  8777  dfac5lem2  9137  axgroth4  9846  rexuz2  11932  4fvwrd4  12653  cshwsexa  13770  divalglem10  15327  divalgb  15329  lsmelval2  19287  tgcmp  21406  hauscmplem  21411  unisngl  21532  xkobval  21591  txtube  21645  txcmplem1  21646  txkgen  21657  xkococnlem  21664  mbfaddlem  23626  mbfsup  23630  elaa  24270  dchrisumlem3  25379  colperpexlem3  25823  midex  25828  iscgra1  25901  ax5seg  26017  edglnl  26237  usgr2pth0  26871  sumdmdii  29583  2reuswap2  29636  unipreima  29755  fpwrelmapffslem  29816  esumfsup  30441  reprdifc  31014  bnj168  31105  bnj1398  31409  cvmliftlem15  31587  dfpo2  31952  ellines  32565  bj-elsngl  33262  bj-dfmpt2a  33377  ptrecube  33722  cnambfre  33771  islshpat  34807  lfl1dim  34911  glbconxN  35167  3dim0  35246  2dim  35259  1dimN  35260  islpln5  35324  islvol5  35368  dalem20  35482  lhpex2leN  35802  mapdval4N  37423  rexrabdioph  37860  rmxdioph  38085  expdiophlem1  38090  imaiun1  38445  coiun1  38446  prmunb2  39012  fourierdlem48  40874  2rmoswap  41690  wtgoldbnnsum4prm  42200  bgoldbnnsum3prm  42202  islindeps2  42782  isldepslvec2  42784
  Copyright terms: Public domain W3C validator