Theorem mpt2eq123 5662

Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Revised by Mario Carneiro, 19-Mar-2015.)

Assertion

Ref	Expression
mpt2eq123	⊢ ((A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F)) → (x ∈ A, y ∈ B ↦ C) = (x ∈ D, y ∈ E ↦ F))

Distinct variable groups:   x,y,A   y,B   x,D,y   y,E

Allowed substitution hints:   B(x)   C(x, y)   E(x)   F(x, y)

Proof of Theorem mpt2eq123

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1619	. . . 4 ⊢ Ⅎx A = D
2		nfra1 2665	. . . 4 ⊢ Ⅎx∀x ∈ A (B = E ∧ ∀y ∈ B C = F)
3	1, 2	nfan 1824	. . 3 ⊢ Ⅎx(A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F))
4		nfv 1619	. . . 4 ⊢ Ⅎy A = D
5		nfcv 2490	. . . . 5 ⊢ ℲyA
6		nfv 1619	. . . . . 6 ⊢ Ⅎy B = E
7		nfra1 2665	. . . . . 6 ⊢ Ⅎy∀y ∈ B C = F
8	6, 7	nfan 1824	. . . . 5 ⊢ Ⅎy(B = E ∧ ∀y ∈ B C = F)
9	5, 8	nfral 2668	. . . 4 ⊢ Ⅎy∀x ∈ A (B = E ∧ ∀y ∈ B C = F)
10	4, 9	nfan 1824	. . 3 ⊢ Ⅎy(A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F))
11		nfv 1619	. . 3 ⊢ Ⅎz(A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F))
12		rsp 2675	. . . . . . 7 ⊢ (∀x ∈ A (B = E ∧ ∀y ∈ B C = F) → (x ∈ A → (B = E ∧ ∀y ∈ B C = F)))
13		rsp 2675	. . . . . . . . . 10 ⊢ (∀y ∈ B C = F → (y ∈ B → C = F))
14		eqeq2 2362	. . . . . . . . . 10 ⊢ (C = F → (z = C ↔ z = F))
15	13, 14	syl6 29	. . . . . . . . 9 ⊢ (∀y ∈ B C = F → (y ∈ B → (z = C ↔ z = F)))
16	15	pm5.32d 620	. . . . . . . 8 ⊢ (∀y ∈ B C = F → ((y ∈ B ∧ z = C) ↔ (y ∈ B ∧ z = F)))
17		eleq2 2414	. . . . . . . . 9 ⊢ (B = E → (y ∈ B ↔ y ∈ E))
18	17	anbi1d 685	. . . . . . . 8 ⊢ (B = E → ((y ∈ B ∧ z = F) ↔ (y ∈ E ∧ z = F)))
19	16, 18	sylan9bbr 681	. . . . . . 7 ⊢ ((B = E ∧ ∀y ∈ B C = F) → ((y ∈ B ∧ z = C) ↔ (y ∈ E ∧ z = F)))
20	12, 19	syl6 29	. . . . . 6 ⊢ (∀x ∈ A (B = E ∧ ∀y ∈ B C = F) → (x ∈ A → ((y ∈ B ∧ z = C) ↔ (y ∈ E ∧ z = F))))
21	20	pm5.32d 620	. . . . 5 ⊢ (∀x ∈ A (B = E ∧ ∀y ∈ B C = F) → ((x ∈ A ∧ (y ∈ B ∧ z = C)) ↔ (x ∈ A ∧ (y ∈ E ∧ z = F))))
22		eleq2 2414	. . . . . 6 ⊢ (A = D → (x ∈ A ↔ x ∈ D))
23	22	anbi1d 685	. . . . 5 ⊢ (A = D → ((x ∈ A ∧ (y ∈ E ∧ z = F)) ↔ (x ∈ D ∧ (y ∈ E ∧ z = F))))
24	21, 23	sylan9bbr 681	. . . 4 ⊢ ((A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F)) → ((x ∈ A ∧ (y ∈ B ∧ z = C)) ↔ (x ∈ D ∧ (y ∈ E ∧ z = F))))
25		anass 630	. . . 4 ⊢ (((x ∈ A ∧ y ∈ B) ∧ z = C) ↔ (x ∈ A ∧ (y ∈ B ∧ z = C)))
26		anass 630	. . . 4 ⊢ (((x ∈ D ∧ y ∈ E) ∧ z = F) ↔ (x ∈ D ∧ (y ∈ E ∧ z = F)))
27	24, 25, 26	3bitr4g 279	. . 3 ⊢ ((A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F)) → (((x ∈ A ∧ y ∈ B) ∧ z = C) ↔ ((x ∈ D ∧ y ∈ E) ∧ z = F)))
28	3, 10, 11, 27	oprabbid 5564	. 2 ⊢ ((A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F)) → {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)} = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ D ∧ y ∈ E) ∧ z = F)})
29		df-mpt2 5655	. 2 ⊢ (x ∈ A, y ∈ B ↦ C) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ z = C)}
30		df-mpt2 5655	. 2 ⊢ (x ∈ D, y ∈ E ↦ F) = {⟨⟨x, y⟩, z⟩ ∣ ((x ∈ D ∧ y ∈ E) ∧ z = F)}
31	28, 29, 30	3eqtr4g 2410	1 ⊢ ((A = D ∧ ∀x ∈ A (B = E ∧ ∀y ∈ B C = F)) → (x ∈ A, y ∈ B ↦ C) = (x ∈ D, y ∈ E ↦ F))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710  ∀wral 2615  {coprab 5528   ↦ cmpt2 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-oprab 5529  df-mpt2 5655

This theorem is used by:  mpt2eq12  5663