oprabid

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker oprabidw when possible. (Contributed by Mario Carneiro, 20-Mar-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	oprabid	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow φ$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨⟨x, y⟩, z⟩ \in V$
2		opex	$⊢ ⟨x, y⟩ \in V$
3		vex	$⊢ z \in V$
4	2 3	eqvinop	$⊢ w = ⟨⟨x, y⟩, z⟩ \leftrightarrow \exists a \exists t (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)$
5	4	biimpi	$⊢ w = ⟨⟨x, y⟩, z⟩ \to \exists a \exists t (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)$
6		eqeq1	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩)$
7		vex	$⊢ a \in V$
8		vex	$⊢ t \in V$
9	7 8	opth1	$⊢ ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩ \to a = ⟨x, y⟩$
10	6 9	syl6bi	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to a = ⟨x, y⟩)$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	eqvinop	$⊢ a = ⟨x, y⟩ \leftrightarrow \exists r \exists s (a = ⟨r, s⟩ \land ⟨r, s⟩ = ⟨x, y⟩)$
14		opeq1	$⊢ a = ⟨r, s⟩ \to ⟨a, t⟩ = ⟨⟨r, s⟩, t⟩$
15	14	eqeq2d	$⊢ a = ⟨r, s⟩ \to (w = ⟨a, t⟩ \leftrightarrow w = ⟨⟨r, s⟩, t⟩)$
16	11 12 3	otth2	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \leftrightarrow (x = r \land y = s \land z = t)$
17		euequ	$⊢ \exists! x x = r$
18		eupick	$⊢ (\exists! x x = r \land \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))) \to (x = r \to \exists y (y = s \land \exists z (z = t \land φ)))$
19	17 18	mpan	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to (x = r \to \exists y (y = s \land \exists z (z = t \land φ)))$
20		euequ	$⊢ \exists! y y = s$
21		eupick	$⊢ (\exists! y y = s \land \exists y (y = s \land \exists z (z = t \land φ))) \to (y = s \to \exists z (z = t \land φ))$
22	20 21	mpan	$⊢ \exists y (y = s \land \exists z (z = t \land φ)) \to (y = s \to \exists z (z = t \land φ))$
23		euequ	$⊢ \exists! z z = t$
24		eupick	$⊢ (\exists! z z = t \land \exists z (z = t \land φ)) \to (z = t \to φ)$
25	23 24	mpan	$⊢ \exists z (z = t \land φ) \to (z = t \to φ)$
26	22 25	syl6	$⊢ \exists y (y = s \land \exists z (z = t \land φ)) \to (y = s \to (z = t \to φ))$
27	19 26	syl6	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to (x = r \to (y = s \to (z = t \to φ)))$
28	27	3impd	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to ((x = r \land y = s \land z = t) \to φ)$
29	16 28	biimtrid	$⊢ \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ))) \to (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \to φ)$
30		df-3an	$⊢ (x = r \land y = s \land z = t) \leftrightarrow ((x = r \land y = s) \land z = t)$
31	16 30	bitri	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \leftrightarrow ((x = r \land y = s) \land z = t)$
32	31	anbi1i	$⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \leftrightarrow (((x = r \land y = s) \land z = t) \land φ)$
33		anass	$⊢ (((x = r \land y = s) \land z = t) \land φ) \leftrightarrow ((x = r \land y = s) \land (z = t \land φ))$
34		anass	$⊢ ((x = r \land y = s) \land (z = t \land φ)) \leftrightarrow (x = r \land (y = s \land (z = t \land φ)))$
35	32 33 34	3bitri	$⊢ (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \leftrightarrow (x = r \land (y = s \land (z = t \land φ)))$
36	35	3exbii	$⊢ \exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ)))$
37		nfcvf2	$⊢ \neg \forall x x = z \to \underline{Ⅎ} z x$
38		nfcvd	$⊢ \neg \forall x x = z \to \underline{Ⅎ} z r$
39	37 38	nfeqd	$⊢ \neg \forall x x = z \to Ⅎ z x = r$
40	39	exdistrf	$⊢ \exists x \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
41	40	eximi	$⊢ \exists y \exists x \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists y \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
42		excom	$⊢ \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ))) \leftrightarrow \exists y \exists x \exists z (x = r \land (y = s \land (z = t \land φ)))$
43		excom	$⊢ \exists x \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \leftrightarrow \exists y \exists x (x = r \land \exists z (y = s \land (z = t \land φ)))$
44	41 42 43	3imtr4i	$⊢ \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x \exists y (x = r \land \exists z (y = s \land (z = t \land φ)))$
45		nfcvf2	$⊢ \neg \forall x x = y \to \underline{Ⅎ} y x$
46		nfcvd	$⊢ \neg \forall x x = y \to \underline{Ⅎ} y r$
47	45 46	nfeqd	$⊢ \neg \forall x x = y \to Ⅎ y x = r$
48	47	exdistrf	$⊢ \exists x \exists y (x = r \land \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ)))$
49		nfcvf2	$⊢ \neg \forall y y = z \to \underline{Ⅎ} z y$
50		nfcvd	$⊢ \neg \forall y y = z \to \underline{Ⅎ} z s$
51	49 50	nfeqd	$⊢ \neg \forall y y = z \to Ⅎ z y = s$
52	51	exdistrf	$⊢ \exists y \exists z (y = s \land (z = t \land φ)) \to \exists y (y = s \land \exists z (z = t \land φ))$
53	52	anim2i	$⊢ (x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \to (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
54	53	eximi	$⊢ \exists x (x = r \land \exists y \exists z (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
55	44 48 54	3syl	$⊢ \exists x \exists y \exists z (x = r \land (y = s \land (z = t \land φ))) \to \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
56	36 55	sylbi	$⊢ \exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to \exists x (x = r \land \exists y (y = s \land \exists z (z = t \land φ)))$
57	29 56	syl11	$⊢ ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \to (\exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to φ)$
58		eqeq1	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨r, s⟩, t⟩ = ⟨⟨x, y⟩, z⟩)$
59		eqcom	$⊢ ⟨⟨r, s⟩, t⟩ = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩$
60	58 59	bitrdi	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \leftrightarrow ⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩)$
61	60	anbi1d	$⊢ w = ⟨⟨r, s⟩, t⟩ \to ((w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ))$
62	61	3exbidv	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ))$
63	62	imbi1d	$⊢ w = ⟨⟨r, s⟩, t⟩ \to ((\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ) \leftrightarrow (\exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to φ))$
64	60 63	imbi12d	$⊢ w = ⟨⟨r, s⟩, t⟩ \to ((w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)) \leftrightarrow (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \to (\exists x \exists y \exists z (⟨⟨x, y⟩, z⟩ = ⟨⟨r, s⟩, t⟩ \land φ) \to φ)))$
65	57 64	mpbiri	$⊢ w = ⟨⟨r, s⟩, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
66	15 65	syl6bi	$⊢ a = ⟨r, s⟩ \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
67	66	adantr	$⊢ (a = ⟨r, s⟩ \land ⟨r, s⟩ = ⟨x, y⟩) \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
68	67	exlimivv	$⊢ \exists r \exists s (a = ⟨r, s⟩ \land ⟨r, s⟩ = ⟨x, y⟩) \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
69	13 68	sylbi	$⊢ a = ⟨x, y⟩ \to (w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
70	69	com3l	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (a = ⟨x, y⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)))$
71	10 70	mpdd	$⊢ w = ⟨a, t⟩ \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
72	71	adantr	$⊢ (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩) \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
73	72	exlimivv	$⊢ \exists a \exists t (w = ⟨a, t⟩ \land ⟨a, t⟩ = ⟨⟨x, y⟩, z⟩) \to (w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ))$
74	5 73	mpcom	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to φ)$
75		19.8a	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
76		19.8a	$⊢ \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
77		19.8a	$⊢ \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
78	75 76 77	3syl	$⊢ (w = ⟨⟨x, y⟩, z⟩ \land φ) \to \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)$
79	78	ex	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (φ \to \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ))$
80	74 79	impbid	$⊢ w = ⟨⟨x, y⟩, z⟩ \to (\exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow φ)$
81		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{w \| \exists x \exists y \exists z (w = ⟨⟨x, y⟩, z⟩ \land φ)\}$
82	1 80 81	elab2	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow φ$

Metamath Proof Explorer

Theorem oprabid

Proof