Theorem mpoeq12 7484

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 2769	. . . . 5 ⊢ 𝐸 = 𝐸
2	1	rgenw 3089	. . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸
3	2	jctr 533	. . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
4	3	ralrimivw 3167	. 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
5		mpoeq123 7483	. 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
6	4, 5	sylan2 604	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ∀wral 3085   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  dffi3  9390  cantnfres  9645  xpsval  17623  monpropd  17793  grpsubpropd2  19111  lsmvalx  19708  lsmpropd  19746  funcrngcsetc  20724  funcringcsetc  20758  psrplusgpropd  22363  d1mat2pmat  22864  txval  23689  cnmptk1p  23810  cnmptk2  23811  xpstopnlem1  23934  rrxmval  25532  madjusmdetlem1  34161  pstmval  34229  qqhval2  34316  lmod1zr  49157  infsubc2d  49724