Theorem mpt2eq12 6872

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 2752	. . . . 5 ⊢ 𝐸 = 𝐸
2	1	rgenw 3054	. . . 4 ⊢ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸
3	2	jctr 566	. . 3 ⊢ (𝐵 = 𝐷 → (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
4	3	ralrimivw 3097	. 2 ⊢ (𝐵 = 𝐷 → ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸))
5		mpt2eq123 6871	. 2 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 (𝐵 = 𝐷 ∧ ∀𝑦 ∈ 𝐵 𝐸 = 𝐸)) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))
6	4, 5	sylan2 492	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐸) = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝐸))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624  ∀wral 3042   ↦ cmpt2 6807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-oprab 6809  df-mpt2 6810

This theorem is referenced by:  dffi3  8494  cantnfres  8739  xpsval  16426  homffval  16543  comfffval  16551  monpropd  16590  natfval  16799  plusffval  17440  grpsubfval  17657  grpsubpropd2  17714  lsmvalx  18246  oppglsm  18249  lsmpropd  18282  dvrfval  18876  scaffval  19075  psrmulr  19578  psrplusgpropd  19800  ipffval  20187  marrepfval  20560  marepvfval  20565  d1mat2pmat  20738  txval  21561  cnmptk1p  21682  cnmptk2  21683  xpstopnlem1  21806  pcofval  23002  rrxmval  23380  madjusmdetlem1  30194  pstmval  30239  qqhval2  30327  mendplusgfval  38249  mendmulrfval  38251  mendvscafval  38254  funcrngcsetc  42500  funcringcsetc  42537  lmod1zr  42784