This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = \{⟨x, y⟩ \| φ\}$
	Assertion	relopabiALT	$⊢ Rel A$

Proof

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