Theorem r19.41v 1760

Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90.

Assertion

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

Distinct variable group:   ps,x

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		anass 439	. . . 4 |- (((x e. A /\ ph) /\ ps) <-> (x e. A /\ (ph /\ ps)))
2	1	exbii 1049	. . 3 |- (E.x((x e. A /\ ph) /\ ps) <-> E.x(x e. A /\ (ph /\ ps)))
3		19.41v 1303	. . 3 |- (E.x((x e. A /\ ph) /\ ps) <-> (E.x(x e. A /\ ph) /\ ps))
4	2, 3	bitr3 175	. 2 |- (E.x(x e. A /\ (ph /\ ps)) <-> (E.x(x e. A /\ ph) /\ ps))
5		df-rex 1647	. 2 |- (E.x e. A (ph /\ ps) <-> E.x(x e. A /\ (ph /\ ps)))
6		df-rex 1647	. . 3 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
7	6	anbi1i 481	. 2 |- ((E.x e. A ph /\ ps) <-> (E.x(x e. A /\ ph) /\ ps))
8	4, 5, 7	3bitr4 183	1 |- (E.x e. A (ph /\ ps) <-> (E.x e. A ph /\ ps))

Syntax hints:   <-> wb 146   /\ wa 223   e. wcel 956  E.wex 978  E.wrex 1643

This theorem is referenced by:  r19.42v 1761  reuxfr 2899  imaco 3493  isomin 3890  isoini 3891  mapsnen 4416  infcvglem1 7164  cnpco 7719  blssex 7806  nmo0 8396  axhcompl 8807  hhcmpl 9008  nmop0 9849  nmfn0 9850  nmcopexlem1 9889  nmcfnexlem1 9918  ntunte 10376  fgsb 10480  fgsb2 10485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain