Theorem prtlem9

Description: Lemma for prter3 . (Contributed by Rodolfo Medina, 25-Sep-2010)

	Ref	Expression
Assertion	prtlem9	|- ( A e. B -> E. x e. B [ x ] .~ = [ A ] .~ )

Proof

Step	Hyp	Ref	Expression
1		risset	|- ( A e. B <-> E. x e. B x = A )
2		eceq1	|- ( x = A -> [ x ] .~ = [ A ] .~ )
3	2	reximi	|- ( E. x e. B x = A -> E. x e. B [ x ] .~ = [ A ] .~ )
4	1 3	sylbi	|- ( A e. B -> E. x e. B [ x ] .~ = [ A ] .~ )