Theorem mpt2eq12 6613

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

Assertion

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

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

Allowed substitution hints:   𝐸(𝑥,𝑦)

Proof of Theorem mpt2eq12

Step	Hyp	Ref	Expression
1		eqid 2610	. . . . 5 ⊢ 𝐸 = 𝐸
2	1	rgenw 2908	. . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸
3	2	jctr 563	. . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
4	3	ralrimivw 2950	. 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
5		mpt2eq123 6612	. 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
6	4, 5	sylan2 490	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ∀wral 2896   ↦ cmpt2 6551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-oprab 6553  df-mpt2 6554

This theorem is referenced by:  dffi3  8220  cantnfres  8457  xpsval  16055  homffval  16173  comfffval  16181  monpropd  16220  natfval  16429  plusffval  17070  grpsubfval  17287  grpsubpropd2  17344  lsmvalx  17877  oppglsm  17880  lsmpropd  17913  dvrfval  18507  scaffval  18704  psrmulr  19205  psrplusgpropd  19427  ipffval  19812  marrepfval  20185  marepvfval  20190  d1mat2pmat  20363  txval  21177  cnmptk1p  21298  cnmptk2  21299  xpstopnlem1  21422  pcofval  22618  rrxmval  22996  madjusmdetlem1  29221  pstmval  29266  qqhval2  29354  mendplusgfval  36774  mendmulrfval  36776  mendvscafval  36779  funcrngcsetc  41790  funcringcsetc  41827  lmod1zr  42076