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

Metamath Proof Explorer

Theorem r19.41v

Description: Restricted quantifier version 19.41v . Version of r19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020)

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

Proof

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