Theorem prtlem11

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 12-Oct-2010)

	Ref	Expression
Assertion	prtlem11	|- ( B e. D -> ( C e. A -> ( B = [ C ] .~ -> B e. ( A /. .~ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eceq1	|- ( x = C -> [ x ] .~ = [ C ] .~ )
2	1	rspceeqv	|- ( ( C e. A /\ B = [ C ] .~ ) -> E. x e. A B = [ x ] .~ )
3		elqsg	|- ( B e. D -> ( B e. ( A /. .~ ) <-> E. x e. A B = [ x ] .~ ) )
4	2 3	syl5ibr	|- ( B e. D -> ( ( C e. A /\ B = [ C ] .~ ) -> B e. ( A /. .~ ) ) )
5	4	expd	|- ( B e. D -> ( C e. A -> ( B = [ C ] .~ -> B e. ( A /. .~ ) ) ) )