Theorem r19.42v 1764

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem r19.42v

Step	Hyp	Ref	Expression
1		r19.41v 1763	. 2 |- (E.x e. A (ps /\ ph) <-> (E.x e. A ps /\ ph))
2		ancom 435	. . 3 |- ((ph /\ ps) <-> (ps /\ ph))
3	2	rexbii 1668	. 2 |- (E.x e. A (ph /\ ps) <-> E.x e. A (ps /\ ph))
4		ancom 435	. 2 |- ((ph /\ E.x e. A ps) <-> (E.x e. A ps /\ ph))
5	1, 3, 4	3bitr4 183	1 |- (E.x e. A (ph /\ ps) <-> (ph /\ E.x e. A ps))

Syntax hints:   <-> wb 146   /\ wa 223  E.wrex 1646

This theorem is referenced by:  ceqsrex2v 1890  2reuswap 1937  iunrab 2596  iunin2 2608  iundif2 2610  elxp2 3203  cnvuni 3301  elunirnALT 3869  f1oiso 3904  trcl 4645  aceq5lem2 4736  rexuz2 6445  axgroth4 8780  sumdmdi 10342  subsp 10554

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