Theorem prtlem12

Description: Lemma for prtex and prter3 . (Contributed by Rodolfo Medina, 13-Oct-2010)

	Ref	Expression
Assertion	prtlem12	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}\to \mathrm{Rel}\underset{\dot{}}{\sim }$$

Proof

Step	Hyp	Ref	Expression
1		relopab	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}$$
2		releq	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}\to \left(\mathrm{Rel}\underset{\dot{}}{\sim }\leftrightarrow \mathrm{Rel}\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}\right)$$
3	1 2	mpbiri	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\exists u\in A\left(x\in u\wedge y\in u\right)\right\}\to \mathrm{Rel}\underset{\dot{}}{\sim }$$