Theorem mpoeq3dva 7231

Description: Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013.)

Hypothesis

Ref	Expression
mpoeq3dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
mpoeq3dva	⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)

Proof of Theorem mpoeq3dva

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpoeq3dva.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
2	1	3expb 1116	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2832	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 581	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7220	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7161	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7161	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2881	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  {coprab 7157   ∈ cmpo 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  mpoeq3ia  7232  mpoeq3dv  7233  ofeq  7411  fmpoco  7790  mapxpen  8683  cantnffval  9126  cantnfres  9140  sadfval  15801  smufval  15826  vdwapfval  16307  comfeq  16976  monpropd  17007  cofuval2  17157  cofuass  17159  cofulid  17160  cofurid  17161  catcisolem  17366  prfval  17449  prf1st  17454  prf2nd  17455  1st2ndprf  17456  xpcpropd  17458  curf1  17475  curfuncf  17488  curf2ndf  17497  grpsubpropd2  18205  mulgpropd  18269  oppglsm  18767  subglsm  18799  lsmpropd  18803  gsumcom2  19095  gsumdixp  19359  psrvscafval  20170  evlslem4  20288  evlslem2  20292  psrplusgpropd  20404  mamures  21001  mpomatmul  21055  mamutpos  21067  dmatmul  21106  dmatcrng  21111  scmatscmiddistr  21117  scmatcrng  21130  1marepvmarrepid  21184  1marepvsma1  21192  mdetrsca2  21213  mdetrlin2  21216  mdetunilem5  21225  mdetunilem6  21226  mdetunilem7  21227  mdetunilem8  21228  mdetunilem9  21229  maduval  21247  maducoeval  21248  maducoeval2  21249  madugsum  21252  madurid  21253  smadiadetglem2  21281  cramerimplem2  21293  mat2pmatghm  21338  mat2pmatmul  21339  m2cpminvid  21361  m2cpminvid2  21363  decpmatid  21378  decpmatmulsumfsupp  21381  monmatcollpw  21387  pmatcollpwscmatlem2  21398  mp2pm2mplem3  21416  mp2pm2mplem4  21417  pm2mpghm  21424  pm2mpmhmlem1  21426  ptval2  22209  cnmpt2t  22281  cnmpt22  22282  cnmptcom  22286  cnmptk2  22294  cnmpt2plusg  22696  istgp2  22699  prdstmdd  22732  cnmpt2vsca  22803  cnmpt2ds  23451  cnmpopc  23532  cnmpt2ip  23851  rrxds  23996  rrxmfval  24009  elntg2  26771  nvmfval  28421  fedgmullem2  31026  mdetpmtr12  31090  madjusmdetlem1  31092  pstmval  31135  sseqval  31646  cvmlift2lem6  32555  cvmlift2lem7  32556  cvmlift2lem12  32561  matunitlindflem1  34903  dvhfvadd  38242  funcrngcsetcALT  44319  rrxlinesc  44771