relopabiv

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

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

Proof

Step	Hyp	Ref	Expression
1		relopabiv.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		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
8	6 1 7	3sstr4i	$⊢ A \subseteq V \times V$
9		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
10	8 9	mpbir	$⊢ Rel A$

Metamath Proof Explorer

Theorem relopabiv

Proof