Theorem mpt2eq12 6715

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 2622	. . . . 5 ⊢ 𝐸 = 𝐸
2	1	rgenw 2924	. . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸
3	2	jctr 565	. . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
4	3	ralrimivw 2967	. 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
5		mpt2eq123 6714	. 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
6	4, 5	sylan2 491	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  ∀wral 2912   ↦ cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  dffi3  8337  cantnfres  8574  xpsval  16232  homffval  16350  comfffval  16358  monpropd  16397  natfval  16606  plusffval  17247  grpsubfval  17464  grpsubpropd2  17521  lsmvalx  18054  oppglsm  18057  lsmpropd  18090  dvrfval  18684  scaffval  18881  psrmulr  19384  psrplusgpropd  19606  ipffval  19993  marrepfval  20366  marepvfval  20371  d1mat2pmat  20544  txval  21367  cnmptk1p  21488  cnmptk2  21489  xpstopnlem1  21612  pcofval  22810  rrxmval  23188  madjusmdetlem1  29893  pstmval  29938  qqhval2  30026  mendplusgfval  37755  mendmulrfval  37757  mendvscafval  37760  funcrngcsetc  41998  funcringcsetc  42035  lmod1zr  42282