Theorem mpteq12dv 5196

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.) Remove dependency on ax-10 2178, ax-12 2215. (Revised by SN and GG, 1-Dec-2023.)

Hypotheses

Ref	Expression
mpteq12dv.1	⊢ (𝜑 → 𝐴 = 𝐶)
mpteq12dv.2	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
mpteq12dv	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem mpteq12dv

Step	Hyp	Ref	Expression
1		mpteq12dv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		mpteq12dv.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
3	2	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	1, 3	mpteq12dva 5195	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5172  df-mpt 5191

This theorem is used by:  mpteq1  5198  mpteq1i  5200  mpteq12i  5206  ovmpt3rab1  7676  offval  7691  offval3  7983  cureq  8872  cantnffval  9646  cnfcomlem  9682  fseqenlem1  10031  dfac12lem1  10150  dfac12r  10153  ackbij2lem2  10245  ackbij2lem3  10246  r1om  10249  indv  12248  ccatfval  14642  swrdval  14715  revval  14833  odzval  16889  vdwpc  17078  restval  17517  prdsval  17546  imasval  17603  qusval  17634  mrcfval  17702  cidfval  17770  monfval  17827  ismon  17828  isepi  17835  idfuval  17971  resfval  17987  resfval2  17988  fucval  18056  homafval  18124  idafval  18152  prfval  18293  prf2fval  18295  curfval  18317  curfpropd  18327  hofval  18346  hof2fval  18349  yonedalem3a  18368  yonedalem4a  18369  yonedalem4c  18371  yonedainv  18375  lubfval  18442  glbfval  18455  ipoval  18624  grpinvfval  19108  grpinvfvalALT  19109  grpinvpropd  19144  mulgnn0gsum  19209  cntzfval  19453  pmtrfval  19583  psgnfval  19633  odfval  19665  odfvalALT  19666  sylow1lem2  19732  sylow1lem4  19734  sylow2blem1  19753  sylow3lem1  19760  sylow3lem2  19761  sylow3lem3  19762  sylow3lem6  19765  pj1fval  19827  vrgpfval  19899  gsum2dlem2  20104  gsum2d2  20107  dprdval  20138  dprd2dlem2  20175  dprd2dlem1  20176  dprd2da  20177  dprd2d2  20179  dpjfval  20190  srgbinom  20376  rgspnval  20780  staffval  21013  lspfval  21163  lsppropd  21208  sraval  21365  isphl  21847  ocvfval  21885  pjfval  21925  uvcfval  22003  aspval  22093  asclfval  22099  ressascl  22117  psrval  22136  psrass1lem  22154  psrmulval  22165  mvrfval  22201  opsrval  22268  mpfrcl  22307  evlsval  22308  selvffval  22340  mhpmulcl  22383  psdffval  22391  coe1mul2  22501  cply1mul  22527  evls1fval  22550  evl1fval  22559  evl1maprhm  22610  mamufval  22620  mvmulfval  22770  marepvfval  22793  submafval  22807  mdetfval  22814  madufval  22865  minmar1fval  22874  mat2pmatfval  22954  cpm2mfval  22980  decpmatmullem  23002  decpmatmulsumfsupp  23004  pm2mpval  23026  pm2mpmhmlem1  23049  pm2mpmhmlem2  23050  chpmatfval  23061  ntrfval  23255  clsfval  23256  neifval  23330  lpfval  23369  ordtval  23420  ordtbas2  23422  ordtcnv  23432  ordtrest  23433  ordtrest2  23435  cnpfval  23465  kqval  23958  fmval  24175  fmf  24177  flffval  24221  fcfval  24265  cnextval  24293  tsmsval2  24362  nmfval  24820  nmpropd  24826  nmpropd2  24827  subgnm  24865  tngnm  24883  nmofval  24946  pi1xfrcnv  25291  iscph  25404  tcphval  25452  limcfval  26106  dvfval  26131  eldv  26132  mdegfval  26294  mdegmullem  26310  mdegpropd  26316  coe1mul3  26331  ig1pval  26408  taylfval  26602  ishlg2  28952  ishlg  28955  mirval  29014  ishpg  29124  lmif  29177  islmib  29179  vtxdgfval  29935  vtxdeqd  29945  grpoinvfval  31011  nmoofval  31251  eigvalfval  32386  ressnm  33412  tocycval  33556  idlsrgval  33921  selvply1rhmlemb  34037  extvval  34049  extvfval  34050  mplvrpmrhm  34065  issply  34079  minplyval  34223  ordtprsval  34436  ordtprsuni  34437  ordtrestNEW  34439  ofcfval  34616  ofcfval3  34620  omsval  34812  sitgval  34851  issibf  34852  sitgfval  34860  signstfv  35079  cvmliftlem5  35876  cvmliftlem15  35885  mvrsval  36092  mrsubffval  36094  elmrsubrn  36107  msubffval  36110  mvhfval  36120  msrfval  36124  fwddifval  36750  fwddifnval  36751  tailfval  36999  bj-imdirvallem  37940  bj-endval  38075  lsatset  39871  lkrfval  39968  pmapfval  40637  pclfvalN  40770  polfvalN  40785  watfvalN  40873  ldilfset  40989  ltrnfset  40998  dilfsetN  41033  trnfsetN  41036  trlfset  41041  trlset  41042  tgrpfset  41625  tendofset  41639  erngfset  41680  erngset  41681  erngfset-rN  41688  erngset-rN  41689  dvafset  41885  diaffval  41911  diafval  41912  dvhfset  41961  docaffvalN  42002  docafvalN  42003  djaffvalN  42014  dibffval  42021  dibfval  42022  dicffval  42055  dicfval  42056  dihffval  42111  dochffval  42230  dochfval  42231  djhffval  42277  lcdfval  42469  mapdffval  42507  mapdfval  42508  hvmapffval  42639  hvmapfval  42640  hdmap1ffval  42676  hdmap1fval  42677  hdmapffval  42707  hdmapfval  42708  hgmapffval  42766  hgmapfval  42767  hlhilset  42815  prjcrvfval  43485  hbtlem1  43972  hbtlem7  43974  cytpval  44051  rfovd  44849  fsovd  44856  fsovcnvlem  44861  dssmapfvd  44865  ntrneibex  44921  mnringvald  45059  ovnval  47377  hspmbllem2  47463  smflimsuplem1  47656  smflimsuplem3  47658  smflimsuplem7  47662  smflimsup  47664  ply1mulgsumlem3  49326  ply1mulgsumlem4  49327  ply1mulgsum  49328  lincval  49347  iinfprg  49993  fucofvalg  50252  precofval3  50305  prcofvalg  50310  lmdfval  50583  cmdfval  50584