Theorem r19.41v 1763

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 1051	. . 3 |- (E.x((x e. A /\ ph) /\ ps) <-> E.x(x e. A /\ (ph /\ ps)))
3		19.41v 1305	. . 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 1650	. 2 |- (E.x e. A (ph /\ ps) <-> E.x(x e. A /\ (ph /\ ps)))
6		df-rex 1650	. . 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 958  E.wex 980  E.wrex 1646

This theorem is referenced by:  r19.42v 1764  reuxfr 2904  imaco 3501  isomin 3899  isoini 3900  mapsnen 4429  infcvglem1 7221  cnpco 7769  blssex 7854  nmo0 8451  axhcompl 8868  hhcmpl 9069  nmop0 9910  nmfn0 9911  nmcopexlem1 9951  nmcfnexlem1 9980  ntunte 10439  fgsb 10570  fgsbOLD 10571  fgsb2 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain