Theorem r19.42v 1767

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 1766	. 2 |- (E.x e. A (ps /\ ph) <-> (E.x e. A ps /\ ph))
2		ancom 437	. . 3 |- ((ph /\ ps) <-> (ps /\ ph))
3	2	rexbii 1671	. 2 |- (E.x e. A (ph /\ ps) <-> E.x e. A (ps /\ ph))
4		ancom 437	. 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 1649

This theorem is referenced by:  ceqsrex2v 1893  2reuswap 1940  iunrab 2600  iunin2 2613  iundif2 2615  elxp2 3209  cnvuni 3307  elunirnALT 3875  f1oiso 3910  trcl 4655  aceq5lem2 4746  rexuz2 6446  axgroth4 8775  sumdmdi 10337  subsp 10540

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain