Theorem relopabiALT

Description: Alternate proof of relopabi (shorter but uses more axioms). (Contributed by Mario Carneiro, 21-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	relopabi.1	$$⊢A=\left\{⟨x,y⟩|\phi \right\}$$
Assertion	relopabiALT	$$⊢\mathrm{Rel}A$$

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	$$⊢A=\left\{⟨x,y⟩|\phi \right\}$$
2		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
3	1 2	eqtri	$$⊢A=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
4		vex	$$⊢x\in \mathrm{V}$$
5		vex	$$⊢y\in \mathrm{V}$$
6	4 5	opelvv	$$⊢⟨x,y⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7		eleq1	$$⊢z=⟨x,y⟩\to \left(z\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow ⟨x,y⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
8	6 7	mpbiri	$$⊢z=⟨x,y⟩\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
9	8	adantr	$$⊢\left(z=⟨x,y⟩\wedge \phi \right)\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
10	9	exlimivv	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\to z\in \left(\mathrm{V}\times \mathrm{V}\right)$$
11	10	abssi	$$⊢\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}\subseteq \mathrm{V}\times \mathrm{V}$$
12	3 11	eqsstri	$$⊢A\subseteq \mathrm{V}\times \mathrm{V}$$
13		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
14	12 13	mpbir	$$⊢\mathrm{Rel}A$$