Theorem bnj1521

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1521.1	|- ( ch -> E. x e. B ph )
	bnj1521.2	|- ( th <-> ( ch /\ x e. B /\ ph ) )
	bnj1521.3	|- ( ch -> A. x ch )
Assertion	bnj1521	|- ( ch -> E. x th )

Proof

Step	Hyp	Ref	Expression
1		bnj1521.1	|- ( ch -> E. x e. B ph )
2		bnj1521.2	|- ( th <-> ( ch /\ x e. B /\ ph ) )
3		bnj1521.3	|- ( ch -> A. x ch )
4	1	bnj1196	|- ( ch -> E. x ( x e. B /\ ph ) )
5	4 2 3	bnj1345	|- ( ch -> E. x th )