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

Theorem r19.35 3001
Description: Restricted quantifier version of 19.35 1692. (Contributed by NM, 20-Sep-2003.)
Assertion
Ref Expression
r19.35  |-  ( E. x  e.  A  (
ph  ->  ps )  <->  ( A. x  e.  A  ph  ->  E. x  e.  A  ps ) )

Proof of Theorem r19.35
StepHypRef Expression
1 r19.26 2981 . . . 4  |-  ( A. x  e.  A  ( ph  /\  -.  ps )  <->  ( A. x  e.  A  ph 
/\  A. x  e.  A  -.  ps ) )
2 annim 423 . . . . 5  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
32ralbii 2885 . . . 4  |-  ( A. x  e.  A  ( ph  /\  -.  ps )  <->  A. x  e.  A  -.  ( ph  ->  ps )
)
4 df-an 369 . . . 4  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  -.  ps )  <->  -.  ( A. x  e.  A  ph 
->  -.  A. x  e.  A  -.  ps )
)
51, 3, 43bitr3i 275 . . 3  |-  ( A. x  e.  A  -.  ( ph  ->  ps )  <->  -.  ( A. x  e.  A  ph  ->  -.  A. x  e.  A  -.  ps ) )
65con2bii 330 . 2  |-  ( ( A. x  e.  A  ph 
->  -.  A. x  e.  A  -.  ps )  <->  -. 
A. x  e.  A  -.  ( ph  ->  ps ) )
7 dfrex2 2905 . . 3  |-  ( E. x  e.  A  ps  <->  -. 
A. x  e.  A  -.  ps )
87imbi2i 310 . 2  |-  ( ( A. x  e.  A  ph 
->  E. x  e.  A  ps )  <->  ( A. x  e.  A  ph  ->  -.  A. x  e.  A  -.  ps ) )
9 dfrex2 2905 . 2  |-  ( E. x  e.  A  (
ph  ->  ps )  <->  -.  A. x  e.  A  -.  ( ph  ->  ps ) )
106, 8, 93bitr4ri 278 1  |-  ( E. x  e.  A  (
ph  ->  ps )  <->  ( A. x  e.  A  ph  ->  E. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367   A.wral 2804   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  r19.36v  3002  r19.37  3003  r19.43  3010  r19.37zv  3913  r19.36zv  3918  iinexg  4597  bndndx  10790  nmobndseqi  25895  nmobndseqiALT  25896
  Copyright terms: Public domain W3C validator