eloprabga

Description: The law of concretion for operation class abstraction. Compare elopab . (Contributed by NM, 14-Sep-1999) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 19-Dec-2013) Avoid ax-10 , ax-11 . (Revised by Wolf Lammen, 15-Oct-2024)

		Ref	Expression
	Hypothesis	eloprabga.1	$⊢ (x = A \land y = B \land z = C) \to (φ \leftrightarrow ψ)$
	Assertion	eloprabga	$⊢ (A \in V \land B \in W \land C \in X) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		eloprabga.1	$⊢ (x = A \land y = B \land z = C) \to (φ \leftrightarrow ψ)$
2		elex	$⊢ A \in V \to A \in V$
3		elex	$⊢ B \in W \to B \in V$
4		elex	$⊢ C \in X \to C \in V$
5		opex	$⊢ ⟨⟨A, B⟩, C⟩ \in V$
6		simpr	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to w = ⟨⟨A, B⟩, C⟩$
7	6	eqeq1d	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨A, B⟩, C⟩ = ⟨⟨x, y⟩, z⟩)$
8		eqcom	$⊢ ⟨⟨A, B⟩, C⟩ = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨x, y⟩, z⟩ = ⟨⟨A, B⟩, C⟩$
9		vex	$⊢ x \in V$
10		vex	$⊢ y \in V$
11		vex	$⊢ z \in V$
12	9 10 11	otth2	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨A, B⟩, C⟩ \leftrightarrow (x = A \land y = B \land z = C)$
13	8 12	bitri	$⊢ ⟨⟨A, B⟩, C⟩ = ⟨⟨x, y⟩, z⟩ \leftrightarrow (x = A \land y = B \land z = C)$
14	7 13	bitrdi	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow (x = A \land y = B \land z = C))$
15	14	anbi1d	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to ((w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow ((x = A \land y = B \land z = C) \land φ))$
16	1	pm5.32i	$⊢ ((x = A \land y = B \land z = C) \land φ) \leftrightarrow ((x = A \land y = B \land z = C) \land ψ)$
17	15 16	bitrdi	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to ((w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow ((x = A \land y = B \land z = C) \land ψ))$
18	17	3exbidv	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z ((x = A \land y = B \land z = C) \land ψ))$
19		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
20	19	eleq2i	$⊢ w \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow w \in \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
21		abid	$⊢ w \in \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\} \leftrightarrow \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
22	20 21	bitr2i	$⊢ \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow w \in \{⟨⟨x, y⟩, z⟩ \| φ\}$
23		eleq1	$⊢ w = ⟨⟨A, B⟩, C⟩ \to (w \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\})$
24	22 23	syl5bb	$⊢ w = ⟨⟨A, B⟩, C⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\})$
25	24	adantl	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\})$
26		19.41vvv	$⊢ \exists x \exists y \exists z ((x = A \land y = B \land z = C) \land ψ) \leftrightarrow (\exists x \exists y \exists z (x = A \land y = B \land z = C) \land ψ)$
27		elisset	$⊢ A \in V \to \exists x x = A$
28		elisset	$⊢ B \in V \to \exists y y = B$
29		elisset	$⊢ C \in V \to \exists z z = C$
30	27 28 29	3anim123i	$⊢ (A \in V \land B \in V \land C \in V) \to (\exists x x = A \land \exists y y = B \land \exists z z = C)$
31		3exdistr	$⊢ \exists x \exists y \exists z (x = A \land y = B \land z = C) \leftrightarrow \exists x (x = A \land \exists y (y = B \land \exists z z = C))$
32		19.41v	$⊢ \exists x (x = A \land \exists y (y = B \land \exists z z = C)) \leftrightarrow (\exists x x = A \land \exists y (y = B \land \exists z z = C))$
33		19.41v	$⊢ \exists y (y = B \land \exists z z = C) \leftrightarrow (\exists y y = B \land \exists z z = C)$
34	33	anbi2i	$⊢ (\exists x x = A \land \exists y (y = B \land \exists z z = C)) \leftrightarrow (\exists x x = A \land (\exists y y = B \land \exists z z = C))$
35	31 32 34	3bitri	$⊢ \exists x \exists y \exists z (x = A \land y = B \land z = C) \leftrightarrow (\exists x x = A \land (\exists y y = B \land \exists z z = C))$
36		3anass	$⊢ (\exists x x = A \land \exists y y = B \land \exists z z = C) \leftrightarrow (\exists x x = A \land (\exists y y = B \land \exists z z = C))$
37	35 36	bitr4i	$⊢ \exists x \exists y \exists z (x = A \land y = B \land z = C) \leftrightarrow (\exists x x = A \land \exists y y = B \land \exists z z = C)$
38	30 37	sylibr	$⊢ (A \in V \land B \in V \land C \in V) \to \exists x \exists y \exists z (x = A \land y = B \land z = C)$
39	38	biantrurd	$⊢ (A \in V \land B \in V \land C \in V) \to (ψ \leftrightarrow (\exists x \exists y \exists z (x = A \land y = B \land z = C) \land ψ))$
40	26 39	bitr4id	$⊢ (A \in V \land B \in V \land C \in V) \to (\exists x \exists y \exists z ((x = A \land y = B \land z = C) \land ψ) \leftrightarrow ψ)$
41	40	adantr	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to (\exists x \exists y \exists z ((x = A \land y = B \land z = C) \land ψ) \leftrightarrow ψ)$
42	18 25 41	3bitr3d	$⊢ ((A \in V \land B \in V \land C \in V) \land w = ⟨⟨A, B⟩, C⟩) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ψ)$
43	42	expcom	$⊢ w = ⟨⟨A, B⟩, C⟩ \to ((A \in V \land B \in V \land C \in V) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ψ))$
44	5 43	vtocle	$⊢ (A \in V \land B \in V \land C \in V) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ψ)$
45	2 3 4 44	syl3an	$⊢ (A \in V \land B \in W \land C \in X) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem eloprabga

Proof