Theorem prtlem9

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

	Ref	Expression
Assertion	prtlem9	$$⊢A\in B\to \exists x\in B\left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		risset	$$⊢A\in B\leftrightarrow \exists x\in Bx=A$$
2		eceq1	$$⊢x=A\to \left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$
3	2	reximi	$$⊢\exists x\in Bx=A\to \exists x\in B\left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$
4	1 3	sylbi	$$⊢A\in B\to \exists x\in B\left[x\right]\underset{\dot{}}{\sim }=\left[A\right]\underset{\dot{}}{\sim }$$