Theorem relopabiv

Description: A class of ordered pairs is a relation. For a version without disjoint variable condition, but a longer proof using ax-13 , see relopabi . (Contributed by BJ, 22-Jul-2023)

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

Proof

Step	Hyp	Ref	Expression
1		relopabiv.1	$$⊢A=\left\{⟨x,y⟩|\phi \right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	pm3.2i	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)$$
5	4	a1i	$$⊢\phi \to \left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)$$
6	5	ssopab2i	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq \left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right\}$$
7		df-xp	$$⊢\mathrm{V}\times \mathrm{V}=\left\{⟨x,y⟩|\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right\}$$
8	6 1 7	3sstr4i	$$⊢A\subseteq \mathrm{V}\times \mathrm{V}$$
9		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
10	8 9	mpbir	$$⊢\mathrm{Rel}A$$