This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r19.41

Description: Restricted quantifier version of 19.41 . See r19.41v for a version with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 1-Nov-2010)

Ref Expression
Hypothesis r19.41.1 
|- F/ x ps
Assertion r19.41 
|- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 r19.41.1 
 |-  F/ x ps
2 df-rex 
 |-  ( E. x e. A ( ph /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
3 anass 
 |-  ( ( ( x e. A /\ ph ) /\ ps ) <-> ( x e. A /\ ( ph /\ ps ) ) )
4 3 exbii 
 |-  ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
5 1 19.41 
 |-  ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
6 df-rex 
 |-  ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
7 6 bicomi 
 |-  ( E. x ( x e. A /\ ph ) <-> E. x e. A ph )
8 5 7 bianbi 
 |-  ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> ( E. x e. A ph /\ ps ) )
9 2 4 8 3bitr2i 
 |-  ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )