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 3090
Description: Restricted quantifier version of 19.42v 1917 (see also 19.42 2104). (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 3087 . 2 (∃𝑥𝐴 (𝜓𝜑) ↔ (∃𝑥𝐴 𝜓𝜑))
2 ancom 466 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
32rexbii 3039 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
4 ancom 466 . 2 ((𝜑 ∧ ∃𝑥𝐴 𝜓) ↔ (∃𝑥𝐴 𝜓𝜑))
51, 3, 43bitr4i 292 1 (∃𝑥𝐴 (𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wrex 2912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-rex 2917
This theorem is referenced by:  ceqsrexbv  3335  ceqsrex2v  3336  2reuswap  3408  2reu5  3414  iunrab  4565  iunin2  4582  iundif2  4585  reusv2lem4  4870  iunopab  5010  elxp2OLD  5131  cnvuni  5307  xpdifid  5560  elunirn  6506  f1oiso  6598  oprabrexex2  7155  oeeu  7680  trcl  8601  dfac5lem2  8944  axgroth4  9651  rexuz2  11736  4fvwrd4  12455  cshwsexa  13564  divalglem10  15119  divalgb  15121  lsmelval2  19079  tgcmp  21198  hauscmplem  21203  unisngl  21324  xkobval  21383  txtube  21437  txcmplem1  21438  txkgen  21449  xkococnlem  21456  mbfaddlem  23421  mbfsup  23425  elaa  24065  dchrisumlem3  25174  colperpexlem3  25618  midex  25623  iscgra1  25696  ax5seg  25812  edglnl  26032  usgr2pth0  26655  sumdmdii  29258  2reuswap2  29312  unipreima  29430  fpwrelmapffslem  29492  esumfsup  30117  reprdifc  30690  bnj168  30783  bnj1398  31087  cvmliftlem15  31265  dfpo2  31631  ellines  32243  bj-elsngl  32940  bj-dfmpt2a  33055  ptrecube  33389  cnambfre  33438  islshpat  34130  lfl1dim  34234  glbconxN  34490  3dim0  34569  2dim  34582  1dimN  34583  islpln5  34647  islvol5  34691  dalem20  34805  lhpex2leN  35125  mapdval4N  36747  rexrabdioph  37184  rmxdioph  37409  expdiophlem1  37414  imaiun1  37769  coiun1  37770  prmunb2  38336  fourierdlem48  40140  2rmoswap  40953  wtgoldbnnsum4prm  41461  bgoldbnnsum3prm  41463  islindeps2  42043  isldepslvec2  42045
  Copyright terms: Public domain W3C validator