ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpteq12dv GIF version

Theorem mpteq12dv 4082
Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12dv.1 (𝜑𝐴 = 𝐶)
mpteq12dv.2 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
mpteq12dv (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dv
StepHypRef Expression
1 mpteq12dv.1 . 2 (𝜑𝐴 = 𝐶)
2 mpteq12dv.2 . . 3 (𝜑𝐵 = 𝐷)
32adantr 276 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
41, 3mpteq12dva 4081 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  wcel 2148  cmpt 4061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-opab 4062  df-mpt 4063
This theorem is referenced by:  mpteq12i  4088  offval  6083  offval3  6128  odzval  12211  restval  12629  grpinvfvalg  12792  grpinvpropdg  12821  opprnegg  13065  ntrfval  13233  clsfval  13234  neifval  13273  cnpfval  13328  cnprcl2k  13339  reldvg  13781  dvfvalap  13783  eldvap  13784
  Copyright terms: Public domain W3C validator