Theorem mpoeq3dva 7527

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 1120	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2751	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 578	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7516	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7453	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7453	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2805	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  {coprab 7449   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-oprab 7452  df-mpo 7453

This theorem is referenced by:  mpoeq3ia  7528  mpoeq3dv  7529  fmpoco  8136  mapxpen  9209  cantnffval  9732  cantnfres  9746  sadfval  16498  smufval  16523  vdwapfval  17018  comfeq  17764  monpropd  17798  cofuval2  17951  cofuass  17953  cofulid  17954  cofurid  17955  catcisolem  18177  prfval  18268  prf1st  18273  prf2nd  18274  1st2ndprf  18275  xpcpropd  18278  curf1  18295  curfuncf  18308  curf2ndf  18317  grpsubpropd2  19086  mulgpropd  19156  oppglsm  19684  subglsm  19715  lsmpropd  19719  gsumcom2  20017  gsumdixp  20342  funcrngcsetcALT  20663  psrvscafval  21991  evlslem4  22123  evlslem2  22126  psrplusgpropd  22258  mamures  22422  mpomatmul  22473  mamutpos  22485  dmatmul  22524  dmatcrng  22529  scmatscmiddistr  22535  scmatcrng  22548  1marepvmarrepid  22602  1marepvsma1  22610  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  mdetunilem6  22644  mdetunilem7  22645  mdetunilem8  22646  mdetunilem9  22647  maduval  22665  maducoeval  22666  maducoeval2  22667  madugsum  22670  madurid  22671  smadiadetglem2  22699  cramerimplem2  22711  mat2pmatghm  22757  mat2pmatmul  22758  m2cpminvid  22780  m2cpminvid2  22782  decpmatid  22797  decpmatmulsumfsupp  22800  monmatcollpw  22806  pmatcollpwscmatlem2  22817  mp2pm2mplem3  22835  mp2pm2mplem4  22836  pm2mpghm  22843  pm2mpmhmlem1  22845  ptval2  23630  cnmpt2t  23702  cnmpt22  23703  cnmptcom  23707  cnmptk2  23715  cnmpt2plusg  24117  istgp2  24120  prdstmdd  24153  cnmpt2vsca  24224  cnmpt2ds  24884  cnmpopc  24974  cnmpt2ip  25301  rrxds  25446  rrxmfval  25459  elntg2  29018  nvmfval  30676  fedgmullem2  33643  mdetpmtr12  33771  madjusmdetlem1  33773  pstmval  33841  sseqval  34353  cvmlift2lem6  35276  cvmlift2lem7  35277  cvmlift2lem12  35282  matunitlindflem1  37576  dvhfvadd  41048  fmpocos  42229  2arymaptfo  48388  rrxlinesc  48469