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		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	1	19.41	|- ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
5	3 4	bitr3i	|- ( E. x ( x e. A /\ ( ph /\ ps ) ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
6		df-rex	|- ( E. x e. A ( ph /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
7		df-rex	|- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
8	7	anbi1i	|- ( ( E. x e. A ph /\ ps ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
9	5 6 8	3bitr4i	|- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )