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

Theorem mpteq12f 3827
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)
Assertion
Ref Expression
mpteq12f ((x A = 𝐶 x A B = 𝐷) → (x AB) = (x 𝐶𝐷))

Proof of Theorem mpteq12f
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 nfa1 1431 . . . 4 xx A = 𝐶
2 nfra1 2349 . . . 4 xx A B = 𝐷
31, 2nfan 1454 . . 3 x(x A = 𝐶 x A B = 𝐷)
4 nfv 1418 . . 3 y(x A = 𝐶 x A B = 𝐷)
5 rsp 2363 . . . . . . 7 (x A B = 𝐷 → (x AB = 𝐷))
65imp 115 . . . . . 6 ((x A B = 𝐷 x A) → B = 𝐷)
76eqeq2d 2048 . . . . 5 ((x A B = 𝐷 x A) → (y = By = 𝐷))
87pm5.32da 425 . . . 4 (x A B = 𝐷 → ((x A y = B) ↔ (x A y = 𝐷)))
9 sp 1398 . . . . . 6 (x A = 𝐶A = 𝐶)
109eleq2d 2104 . . . . 5 (x A = 𝐶 → (x Ax 𝐶))
1110anbi1d 438 . . . 4 (x A = 𝐶 → ((x A y = 𝐷) ↔ (x 𝐶 y = 𝐷)))
128, 11sylan9bbr 436 . . 3 ((x A = 𝐶 x A B = 𝐷) → ((x A y = B) ↔ (x 𝐶 y = 𝐷)))
133, 4, 12opabbid 3812 . 2 ((x A = 𝐶 x A B = 𝐷) → {⟨x, y⟩ ∣ (x A y = B)} = {⟨x, y⟩ ∣ (x 𝐶 y = 𝐷)})
14 df-mpt 3810 . 2 (x AB) = {⟨x, y⟩ ∣ (x A y = B)}
15 df-mpt 3810 . 2 (x 𝐶𝐷) = {⟨x, y⟩ ∣ (x 𝐶 y = 𝐷)}
1613, 14, 153eqtr4g 2094 1 ((x A = 𝐶 x A B = 𝐷) → (x AB) = (x 𝐶𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wal 1240   = wceq 1242   wcel 1390  wral 2300  {copab 3807  cmpt 3808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-ral 2305  df-opab 3809  df-mpt 3810
This theorem is referenced by:  mpteq12dva  3828  mpteq12  3830  mpteq2ia  3833  mpteq2da  3836
  Copyright terms: Public domain W3C validator