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

Theorem r19.41v 2942
Description: Restricted quantifier version 19.41v 1830. Version of r19.41 2943 with a dv condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduced dependencies on axioms. (Revised by BJ, 29-Mar-2020.)
Assertion
Ref Expression
r19.41v  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem r19.41v
StepHypRef Expression
1 anass 655 . . . 4  |-  ( ( ( x  e.  A  /\  ph )  /\  ps ) 
<->  ( x  e.  A  /\  ( ph  /\  ps ) ) )
21exbii 1718 . . 3  |-  ( E. x ( ( x  e.  A  /\  ph )  /\  ps )  <->  E. x
( x  e.  A  /\  ( ph  /\  ps ) ) )
3 19.41v 1830 . . 3  |-  ( E. x ( ( x  e.  A  /\  ph )  /\  ps )  <->  ( E. x ( x  e.  A  /\  ph )  /\  ps ) )
42, 3bitr3i 255 . 2  |-  ( E. x ( x  e.  A  /\  ( ph  /\ 
ps ) )  <->  ( E. x ( x  e.  A  /\  ph )  /\  ps ) )
5 df-rex 2743 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x ( x  e.  A  /\  ( ph  /\ 
ps ) ) )
6 df-rex 2743 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
76anbi1i 701 . 2  |-  ( ( E. x  e.  A  ph 
/\  ps )  <->  ( E. x ( x  e.  A  /\  ph )  /\  ps ) )
84, 5, 73bitr4i 281 1  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  ( E. x  e.  A  ph 
/\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    /\ wa 371   E.wex 1663    e. wcel 1887   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-rex 2743
This theorem is referenced by:  r19.41vv  2944  r19.42v  2945  3reeanv  2959  reuind  3243  iuncom4  4286  dfiun2g  4310  iunxiun  4364  inuni  4565  reuxfrd  4625  xpiundi  4889  xpiundir  4890  imaco  5340  coiun  5345  abrexco  6149  imaiun  6150  isomin  6228  isoini  6229  oarec  7263  mapsnen  7647  genpass  9434  4fvwrd4  11909  4sqlem12  14900  imasleval  15447  lsmspsn  18307  utoptop  21249  metrest  21539  metust  21573  cfilucfil  21574  metuel2  21580  istrkg2ld  24508  axsegcon  24957  usgreg2spot  25795  nmoo0  26432  hhcmpl  26853  nmop0  27639  nmfn0  27640  reuxfr4d  28126  rexunirn  28127  ordtconlem1  28730  dya2icoseg2  29100  dya2iocnei  29104  omssubaddlem  29127  omssubadd  29128  omssubaddlemOLD  29131  omssubaddOLD  29132  nofulllem5  30595  bj-mpt2mptALT  31631  mptsnunlem  31740  rabiun  31926  iundif1  31927  poimir  31973  ismblfin  31981  prtlem11  32438  prter2  32453  prter3  32454  islshpat  32583  lshpsmreu  32675  islpln5  33100  islvol5  33144  cdlemftr3  34132  dvhb1dimN  34553  dib1dim  34733  mapdpglem3  35243  hdmapglem7a  35498  diophrex  35618  mapsnend  37480
  Copyright terms: Public domain W3C validator