eqvinot

Description: A variable introduction law for ordered triples, analogous to eqvinop . (Contributed by BTernaryTau, 8-Sep-2026)

	Ref	Expression
Hypotheses	eqvinot.1	$⊢ B \in V$
	eqvinot.2	$⊢ C \in V$
	eqvinot.3	$⊢ D \in V$
Assertion	eqvinot	$⊢ A = ⟨B, C, D⟩ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩)$

Proof

Step	Hyp	Ref	Expression
1		eqvinot.1	$⊢ B \in V$
2		eqvinot.2	$⊢ C \in V$
3		eqvinot.3	$⊢ D \in V$
4		19.42v	$⊢ \exists y (x = B \land (y = C \land A = ⟨x, y, D⟩)) \leftrightarrow (x = B \land \exists y (y = C \land A = ⟨x, y, D⟩))$
5		19.42v	$⊢ \exists z ((x = B \land y = C) \land (z = D \land A = ⟨x, y, z⟩)) \leftrightarrow ((x = B \land y = C) \land \exists z (z = D \land A = ⟨x, y, z⟩))$
6		vex	$⊢ x \in V$
7		vex	$⊢ y \in V$
8		vex	$⊢ z \in V$
9	6 7 8	otth	$⊢ ⟨x, y, z⟩ = ⟨B, C, D⟩ \leftrightarrow (x = B \land y = C \land z = D)$
10	9	anbi2i	$⊢ (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩) \leftrightarrow (A = ⟨x, y, z⟩ \land (x = B \land y = C \land z = D))$
11		ancom	$⊢ (A = ⟨x, y, z⟩ \land (x = B \land y = C \land z = D)) \leftrightarrow ((x = B \land y = C \land z = D) \land A = ⟨x, y, z⟩)$
12		3an4anass	$⊢ ((x = B \land y = C \land z = D) \land A = ⟨x, y, z⟩) \leftrightarrow ((x = B \land y = C) \land (z = D \land A = ⟨x, y, z⟩))$
13	10 11 12	3bitrri	$⊢ ((x = B \land y = C) \land (z = D \land A = ⟨x, y, z⟩)) \leftrightarrow (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩)$
14	13	exbii	$⊢ \exists z ((x = B \land y = C) \land (z = D \land A = ⟨x, y, z⟩)) \leftrightarrow \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩)$
15		oteq3	$⊢ z = D \to ⟨x, y, z⟩ = ⟨x, y, D⟩$
16	15	eqeq2d	$⊢ z = D \to (A = ⟨x, y, z⟩ \leftrightarrow A = ⟨x, y, D⟩)$
17	3 16	ceqsexv	$⊢ \exists z (z = D \land A = ⟨x, y, z⟩) \leftrightarrow A = ⟨x, y, D⟩$
18	17	anbi2i	$⊢ ((x = B \land y = C) \land \exists z (z = D \land A = ⟨x, y, z⟩)) \leftrightarrow ((x = B \land y = C) \land A = ⟨x, y, D⟩)$
19	5 14 18	3bitr3i	$⊢ \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩) \leftrightarrow ((x = B \land y = C) \land A = ⟨x, y, D⟩)$
20		anass	$⊢ ((x = B \land y = C) \land A = ⟨x, y, D⟩) \leftrightarrow (x = B \land (y = C \land A = ⟨x, y, D⟩))$
21	19 20	bitr2i	$⊢ (x = B \land (y = C \land A = ⟨x, y, D⟩)) \leftrightarrow \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩)$
22	21	exbii	$⊢ \exists y (x = B \land (y = C \land A = ⟨x, y, D⟩)) \leftrightarrow \exists y \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩)$
23		oteq2	$⊢ y = C \to ⟨x, y, D⟩ = ⟨x, C, D⟩$
24	23	eqeq2d	$⊢ y = C \to (A = ⟨x, y, D⟩ \leftrightarrow A = ⟨x, C, D⟩)$
25	2 24	ceqsexv	$⊢ \exists y (y = C \land A = ⟨x, y, D⟩) \leftrightarrow A = ⟨x, C, D⟩$
26	25	anbi2i	$⊢ (x = B \land \exists y (y = C \land A = ⟨x, y, D⟩)) \leftrightarrow (x = B \land A = ⟨x, C, D⟩)$
27	4 22 26	3bitr3i	$⊢ \exists y \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩) \leftrightarrow (x = B \land A = ⟨x, C, D⟩)$
28	27	exbii	$⊢ \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩) \leftrightarrow \exists x (x = B \land A = ⟨x, C, D⟩)$
29		oteq1	$⊢ x = B \to ⟨x, C, D⟩ = ⟨B, C, D⟩$
30	29	eqeq2d	$⊢ x = B \to (A = ⟨x, C, D⟩ \leftrightarrow A = ⟨B, C, D⟩)$
31	1 30	ceqsexv	$⊢ \exists x (x = B \land A = ⟨x, C, D⟩) \leftrightarrow A = ⟨B, C, D⟩$
32	28 31	bitr2i	$⊢ A = ⟨B, C, D⟩ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land ⟨x, y, z⟩ = ⟨B, C, D⟩)$

Metamath Proof Explorer

Theorem eqvinot

Proof