Theorem mpoeq12 7326

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

Assertion

Ref	Expression
mpoeq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦

Allowed substitution hints:   𝐸(𝑥,𝑦)

Proof of Theorem mpoeq12

Step	Hyp	Ref	Expression
1		eqid 2738	. . . . 5 ⊢ 𝐸 = 𝐸
2	1	rgenw 3075	. . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸
3	2	jctr 524	. . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
4	3	ralrimivw 3108	. 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
5		mpoeq123 7325	. 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
6	4, 5	sylan2 592	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∀wral 3063   ∈ cmpo 7257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  dffi3  9120  cantnfres  9365  xpsval  17198  monpropd  17366  grpsubpropd2  18596  lsmvalx  19159  lsmpropd  19198  psrplusgpropd  21317  d1mat2pmat  21796  txval  22623  cnmptk1p  22744  cnmptk2  22745  xpstopnlem1  22868  rrxmval  24474  madjusmdetlem1  31679  pstmval  31747  qqhval2  31832  funcrngcsetc  45444  funcringcsetc  45481  lmod1zr  45722