relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Avoid ax-11 and ax-12 . (Revised by SN, 26-Oct-2026)

		Ref	Expression
	Hypothesis	relopabi.1	$⊢ A = \{⟨x, y⟩ \| φ\}$
	Assertion	relopabi	$⊢ Rel A$

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	$⊢ A = \{⟨x, y⟩ \| φ\}$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	pm3.2i	$⊢ (x \in V \land y \in V)$
5	4	a1i	$⊢ φ \to (x \in V \land y \in V)$
6	5	ssopab2i	$⊢ \{⟨x, y⟩ \| φ\} \subseteq \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
7		ax6evr	$⊢ \exists u x = u$
8		ax6evr	$⊢ \exists v y = v$
9		opeq12	$⊢ (x = u \land y = v) \to ⟨x, y⟩ = ⟨u, v⟩$
10	9	eqeq2d	$⊢ (x = u \land y = v) \to (z = ⟨x, y⟩ \leftrightarrow z = ⟨u, v⟩)$
11	10	biimpd	$⊢ (x = u \land y = v) \to (z = ⟨x, y⟩ \to z = ⟨u, v⟩)$
12	11	ex	$⊢ x = u \to (y = v \to (z = ⟨x, y⟩ \to z = ⟨u, v⟩))$
13	12	eximdv	$⊢ x = u \to (\exists v y = v \to \exists v (z = ⟨x, y⟩ \to z = ⟨u, v⟩))$
14	8 13	mpi	$⊢ x = u \to \exists v (z = ⟨x, y⟩ \to z = ⟨u, v⟩)$
15		19.37imv	$⊢ \exists v (z = ⟨x, y⟩ \to z = ⟨u, v⟩) \to (z = ⟨x, y⟩ \to \exists v z = ⟨u, v⟩)$
16	14 15	syl	$⊢ x = u \to (z = ⟨x, y⟩ \to \exists v z = ⟨u, v⟩)$
17	7 16	eximii	$⊢ \exists u (z = ⟨x, y⟩ \to \exists v z = ⟨u, v⟩)$
18	17	19.37iv	$⊢ z = ⟨x, y⟩ \to \exists u \exists v z = ⟨u, v⟩$
19	18	exlimivv	$⊢ \exists x \exists y z = ⟨x, y⟩ \to \exists u \exists v z = ⟨u, v⟩$
20	19	ss2abi	$⊢ \{z \| \exists x \exists y z = ⟨x, y⟩\} \subseteq \{z \| \exists u \exists v z = ⟨u, v⟩\}$
21	4	biantru	$⊢ z = ⟨x, y⟩ \leftrightarrow (z = ⟨x, y⟩ \land (x \in V \land y \in V))$
22	21	2exbii	$⊢ \exists x \exists y z = ⟨x, y⟩ \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V))$
23	22	abbii	$⊢ \{z \| \exists x \exists y z = ⟨x, y⟩\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V))\}$
24		vex	$⊢ u \in V$
25		vex	$⊢ v \in V$
26	24 25	pm3.2i	$⊢ (u \in V \land v \in V)$
27	26	biantru	$⊢ z = ⟨u, v⟩ \leftrightarrow (z = ⟨u, v⟩ \land (u \in V \land v \in V))$
28	27	2exbii	$⊢ \exists u \exists v z = ⟨u, v⟩ \leftrightarrow \exists u \exists v (z = ⟨u, v⟩ \land (u \in V \land v \in V))$
29	28	abbii	$⊢ \{z \| \exists u \exists v z = ⟨u, v⟩\} = \{z \| \exists u \exists v (z = ⟨u, v⟩ \land (u \in V \land v \in V))\}$
30	20 23 29	3sstr3i	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V))\} \subseteq \{z \| \exists u \exists v (z = ⟨u, v⟩ \land (u \in V \land v \in V))\}$
31		df-opab	$⊢ \{⟨x, y⟩ \| (x \in V \land y \in V)\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V))\}$
32		df-opab	$⊢ \{⟨u, v⟩ \| (u \in V \land v \in V)\} = \{z \| \exists u \exists v (z = ⟨u, v⟩ \land (u \in V \land v \in V))\}$
33	30 31 32	3sstr4i	$⊢ \{⟨x, y⟩ \| (x \in V \land y \in V)\} \subseteq \{⟨u, v⟩ \| (u \in V \land v \in V)\}$
34		df-xp	$⊢ V \times V = \{⟨u, v⟩ \| (u \in V \land v \in V)\}$
35	33 34	sseqtrri	$⊢ \{⟨x, y⟩ \| (x \in V \land y \in V)\} \subseteq V \times V$
36	6 35	sstri	$⊢ \{⟨x, y⟩ \| φ\} \subseteq V \times V$
37	1 36	eqsstri	$⊢ A \subseteq V \times V$
38		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
39	37 38	mpbir	$⊢ Rel A$

Metamath Proof Explorer

Theorem relopabi

Proof