cotsexgw

Description: Substitution of class A for ordered triple <. x , y , z >. , analogous to copsexgw . (Contributed by BTernaryTau, 8-Sep-2026)

		Ref	Expression
	Assertion	cotsexgw	$⊢ A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ))$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3		vex	$⊢ z \in V$
4	1 2 3	eqvinot	$⊢ A = ⟨x, y, z⟩ \leftrightarrow \exists u \exists v \exists w (A = ⟨u, v, w⟩ \land ⟨u, v, w⟩ = ⟨x, y, z⟩)$
5		19.8a	$⊢ (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \to \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ)$
6	5	19.8ad	$⊢ (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \to \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ)$
7	6	19.8ad	$⊢ (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \to \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ)$
8	7	ex	$⊢ ⟨u, v, w⟩ = ⟨x, y, z⟩ \to (φ \to \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ))$
9		vex	$⊢ u \in V$
10		vex	$⊢ v \in V$
11		vex	$⊢ w \in V$
12	9 10 11	otth	$⊢ ⟨u, v, w⟩ = ⟨x, y, z⟩ \leftrightarrow (u = x \land v = y \land w = z)$
13	12	anbi1i	$⊢ (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \leftrightarrow ((u = x \land v = y \land w = z) \land φ)$
14	13	3exbii	$⊢ \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z ((u = x \land v = y \land w = z) \land φ)$
15		3an4anass	$⊢ ((u = x \land v = y \land w = z) \land φ) \leftrightarrow ((u = x \land v = y) \land (w = z \land φ))$
16	15	exbii	$⊢ \exists z ((u = x \land v = y \land w = z) \land φ) \leftrightarrow \exists z ((u = x \land v = y) \land (w = z \land φ))$
17		19.42v	$⊢ \exists z ((u = x \land v = y) \land (w = z \land φ)) \leftrightarrow ((u = x \land v = y) \land \exists z (w = z \land φ))$
18	16 17	bitri	$⊢ \exists z ((u = x \land v = y \land w = z) \land φ) \leftrightarrow ((u = x \land v = y) \land \exists z (w = z \land φ))$
19	18	exbii	$⊢ \exists y \exists z ((u = x \land v = y \land w = z) \land φ) \leftrightarrow \exists y ((u = x \land v = y) \land \exists z (w = z \land φ))$
20		anass	$⊢ ((u = x \land v = y) \land \exists z (w = z \land φ)) \leftrightarrow (u = x \land (v = y \land \exists z (w = z \land φ)))$
21	20	exbii	$⊢ \exists y ((u = x \land v = y) \land \exists z (w = z \land φ)) \leftrightarrow \exists y (u = x \land (v = y \land \exists z (w = z \land φ)))$
22		19.42v	$⊢ \exists y (u = x \land (v = y \land \exists z (w = z \land φ))) \leftrightarrow (u = x \land \exists y (v = y \land \exists z (w = z \land φ)))$
23	19 21 22	3bitri	$⊢ \exists y \exists z ((u = x \land v = y \land w = z) \land φ) \leftrightarrow (u = x \land \exists y (v = y \land \exists z (w = z \land φ)))$
24	23	exbii	$⊢ \exists x \exists y \exists z ((u = x \land v = y \land w = z) \land φ) \leftrightarrow \exists x (u = x \land \exists y (v = y \land \exists z (w = z \land φ)))$
25		ax12ev2c	$⊢ u = x \to (\exists x (u = x \land \exists y (v = y \land \exists z (w = z \land φ))) \to \exists y (v = y \land \exists z (w = z \land φ)))$
26		ax12ev2c	$⊢ v = y \to (\exists y (v = y \land \exists z (w = z \land φ)) \to \exists z (w = z \land φ))$
27		ax12ev2c	$⊢ w = z \to (\exists z (w = z \land φ) \to φ)$
28	26 27	sylan9	$⊢ (v = y \land w = z) \to (\exists y (v = y \land \exists z (w = z \land φ)) \to φ)$
29	25 28	sylan9	$⊢ (u = x \land (v = y \land w = z)) \to (\exists x (u = x \land \exists y (v = y \land \exists z (w = z \land φ))) \to φ)$
30	29	3impb	$⊢ (u = x \land v = y \land w = z) \to (\exists x (u = x \land \exists y (v = y \land \exists z (w = z \land φ))) \to φ)$
31	24 30	biimtrid	$⊢ (u = x \land v = y \land w = z) \to (\exists x \exists y \exists z ((u = x \land v = y \land w = z) \land φ) \to φ)$
32	14 31	biimtrid	$⊢ (u = x \land v = y \land w = z) \to (\exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \to φ)$
33	12 32	sylbi	$⊢ ⟨u, v, w⟩ = ⟨x, y, z⟩ \to (\exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ) \to φ)$
34	8 33	impbid	$⊢ ⟨u, v, w⟩ = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ))$
35		eqeq1	$⊢ A = ⟨u, v, w⟩ \to (A = ⟨x, y, z⟩ \leftrightarrow ⟨u, v, w⟩ = ⟨x, y, z⟩)$
36	35	anbi1d	$⊢ A = ⟨u, v, w⟩ \to ((A = ⟨x, y, z⟩ \land φ) \leftrightarrow (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ))$
37	36	3exbidv	$⊢ A = ⟨u, v, w⟩ \to (\exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ))$
38	37	bibi2d	$⊢ A = ⟨u, v, w⟩ \to ((φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ)) \leftrightarrow (φ \leftrightarrow \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ)))$
39	35 38	imbi12d	$⊢ A = ⟨u, v, w⟩ \to ((A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ))) \leftrightarrow (⟨u, v, w⟩ = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (⟨u, v, w⟩ = ⟨x, y, z⟩ \land φ))))$
40	34 39	mpbiri	$⊢ A = ⟨u, v, w⟩ \to (A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ)))$
41	40	adantr	$⊢ (A = ⟨u, v, w⟩ \land ⟨u, v, w⟩ = ⟨x, y, z⟩) \to (A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ)))$
42	41	exlimiv	$⊢ \exists w (A = ⟨u, v, w⟩ \land ⟨u, v, w⟩ = ⟨x, y, z⟩) \to (A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ)))$
43	42	exlimivv	$⊢ \exists u \exists v \exists w (A = ⟨u, v, w⟩ \land ⟨u, v, w⟩ = ⟨x, y, z⟩) \to (A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ)))$
44	4 43	sylbi	$⊢ A = ⟨x, y, z⟩ \to (A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ)))$
45	44	pm2.43i	$⊢ A = ⟨x, y, z⟩ \to (φ \leftrightarrow \exists x \exists y \exists z (A = ⟨x, y, z⟩ \land φ))$

Metamath Proof Explorer

Theorem cotsexgw

Proof