Theorem mpoeq123dva 7507

Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)

Hypotheses

Ref	Expression
mpoeq123dv.1	⊢ (𝜑 → 𝐴 = 𝐷)
mpoeq123dva.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
mpoeq123dva.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)

Assertion

Ref	Expression
mpoeq123dva	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpoeq123dva

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpoeq123dva.3	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹)
2	1	eqeq2d 2746	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐹))
3	2	pm5.32da 579	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐹)))
4		mpoeq123dva.2	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸)
5	4	eleq2d 2825	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐸))
6	5	pm5.32da 579	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐸)))
7		mpoeq123dv.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 = 𝐷)
8	7	eleq2d 2825	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐷))
9	8	anbi1d 631	. . . . . 6 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐸) ↔ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸)))
10	6, 9	bitrd 279	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸)))
11	10	anbi1d 631	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐹) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹)))
12	3, 11	bitrd 279	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹)))
13	12	oprabbidv 7499	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹)})
14		df-mpo 7436	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
15		df-mpo 7436	. 2 ⊢ (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸) ∧ 𝑧 = 𝐹)}
16	13, 14, 15	3eqtr4g 2800	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  {coprab 7432   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  mpoeq123dv  7508  natpropd  18033  fucpropd  18034  curfpropd  18290  hofpropd  18324  rngcifuestrc  20656  funcrngcsetc  20657  funcrngcsetcALT  20658  funcringcsetc  20691  rrxdsfi  25459  eengv  29009  elntg  29014  submat1n  33766  rrxtopnfi  46243  eenglngeehlnm  48589