Theorem mpoeq3dva 7486

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 1121	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐷)
3	2	eqeq2d 2744	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑧 = 𝐶 ↔ 𝑧 = 𝐷))
4	3	pm5.32da 580	. . 3 ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)))
5	4	oprabbidv 7475	. 2 ⊢ (𝜑 → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)})
6		df-mpo 7414	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
7		df-mpo 7414	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐷)}
8	5, 6, 7	3eqtr4g 2798	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {coprab 7410   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-oprab 7413  df-mpo 7414

This theorem is referenced by:  mpoeq3ia  7487  mpoeq3dv  7488  fmpoco  8081  mapxpen  9143  cantnffval  9658  cantnfres  9672  sadfval  16393  smufval  16418  vdwapfval  16904  comfeq  17650  monpropd  17684  cofuval2  17837  cofuass  17839  cofulid  17840  cofurid  17841  catcisolem  18060  prfval  18151  prf1st  18156  prf2nd  18157  1st2ndprf  18158  xpcpropd  18161  curf1  18178  curfuncf  18191  curf2ndf  18200  grpsubpropd2  18929  mulgpropd  18996  oppglsm  19510  subglsm  19541  lsmpropd  19545  gsumcom2  19843  gsumdixp  20131  psrvscafval  21509  evlslem4  21637  evlslem2  21642  psrplusgpropd  21758  mamures  21892  mpomatmul  21948  mamutpos  21960  dmatmul  21999  dmatcrng  22004  scmatscmiddistr  22010  scmatcrng  22023  1marepvmarrepid  22077  1marepvsma1  22085  mdetrsca2  22106  mdetrlin2  22109  mdetunilem5  22118  mdetunilem6  22119  mdetunilem7  22120  mdetunilem8  22121  mdetunilem9  22122  maduval  22140  maducoeval  22141  maducoeval2  22142  madugsum  22145  madurid  22146  smadiadetglem2  22174  cramerimplem2  22186  mat2pmatghm  22232  mat2pmatmul  22233  m2cpminvid  22255  m2cpminvid2  22257  decpmatid  22272  decpmatmulsumfsupp  22275  monmatcollpw  22281  pmatcollpwscmatlem2  22292  mp2pm2mplem3  22310  mp2pm2mplem4  22311  pm2mpghm  22318  pm2mpmhmlem1  22320  ptval2  23105  cnmpt2t  23177  cnmpt22  23178  cnmptcom  23182  cnmptk2  23190  cnmpt2plusg  23592  istgp2  23595  prdstmdd  23628  cnmpt2vsca  23699  cnmpt2ds  24359  cnmpopc  24444  cnmpt2ip  24765  rrxds  24910  rrxmfval  24923  elntg2  28243  nvmfval  29897  fedgmullem2  32715  mdetpmtr12  32805  madjusmdetlem1  32807  pstmval  32875  sseqval  33387  cvmlift2lem6  34299  cvmlift2lem7  34300  cvmlift2lem12  34305  matunitlindflem1  36484  dvhfvadd  39962  fmpocos  41056  funcrngcsetcALT  46897  2arymaptfo  47340  rrxlinesc  47421