Theorem opabid2

Description: A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006)

	Ref	Expression
Assertion	opabid2	$$⊢\mathrm{Rel}A\to \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢z\in \mathrm{V}$$
2		vex	$$⊢w\in \mathrm{V}$$
3		opeq1	$$⊢x=z\to ⟨x,y⟩=⟨z,y⟩$$
4	3	eleq1d	$$⊢x=z\to \left(⟨x,y⟩\in A\leftrightarrow ⟨z,y⟩\in A\right)$$
5		opeq2	$$⊢y=w\to ⟨z,y⟩=⟨z,w⟩$$
6	5	eleq1d	$$⊢y=w\to \left(⟨z,y⟩\in A\leftrightarrow ⟨z,w⟩\in A\right)$$
7	1 2 4 6	opelopab	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}\leftrightarrow ⟨z,w⟩\in A$$
8	7	gen2	$$⊢\forall z\forall w\left(⟨z,w⟩\in \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}\leftrightarrow ⟨z,w⟩\in A\right)$$
9		relopabv	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|⟨x,y⟩\in A\right\}$$
10		eqrel	$$⊢\left(\mathrm{Rel}\left\{⟨x,y⟩|⟨x,y⟩\in A\right\}\wedge \mathrm{Rel}A\right)\to \left(\left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=A\leftrightarrow \forall z\forall w\left(⟨z,w⟩\in \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}\leftrightarrow ⟨z,w⟩\in A\right)\right)$$
11	9 10	mpan	$$⊢\mathrm{Rel}A\to \left(\left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=A\leftrightarrow \forall z\forall w\left(⟨z,w⟩\in \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}\leftrightarrow ⟨z,w⟩\in A\right)\right)$$
12	8 11	mpbiri	$$⊢\mathrm{Rel}A\to \left\{⟨x,y⟩|⟨x,y⟩\in A\right\}=A$$