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

Theorem cbvmpt 3842
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.)
Hypotheses
Ref Expression
cbvmpt.1 yB
cbvmpt.2 x𝐶
cbvmpt.3 (x = yB = 𝐶)
Assertion
Ref Expression
cbvmpt (x AB) = (y A𝐶)
Distinct variable groups:   x,A   y,A
Allowed substitution hints:   B(x,y)   𝐶(x,y)

Proof of Theorem cbvmpt
Dummy variables z w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1418 . . . 4 w(x A z = B)
2 nfv 1418 . . . . 5 x w A
3 nfs1v 1812 . . . . 5 x[w / x]z = B
42, 3nfan 1454 . . . 4 x(w A [w / x]z = B)
5 eleq1 2097 . . . . 5 (x = w → (x Aw A))
6 sbequ12 1651 . . . . 5 (x = w → (z = B ↔ [w / x]z = B))
75, 6anbi12d 442 . . . 4 (x = w → ((x A z = B) ↔ (w A [w / x]z = B)))
81, 4, 7cbvopab1 3821 . . 3 {⟨x, z⟩ ∣ (x A z = B)} = {⟨w, z⟩ ∣ (w A [w / x]z = B)}
9 nfv 1418 . . . . 5 y w A
10 cbvmpt.1 . . . . . . 7 yB
1110nfeq2 2186 . . . . . 6 y z = B
1211nfsb 1819 . . . . 5 y[w / x]z = B
139, 12nfan 1454 . . . 4 y(w A [w / x]z = B)
14 nfv 1418 . . . 4 w(y A z = 𝐶)
15 eleq1 2097 . . . . 5 (w = y → (w Ay A))
16 sbequ 1718 . . . . . 6 (w = y → ([w / x]z = B ↔ [y / x]z = B))
17 cbvmpt.2 . . . . . . . 8 x𝐶
1817nfeq2 2186 . . . . . . 7 x z = 𝐶
19 cbvmpt.3 . . . . . . . 8 (x = yB = 𝐶)
2019eqeq2d 2048 . . . . . . 7 (x = y → (z = Bz = 𝐶))
2118, 20sbie 1671 . . . . . 6 ([y / x]z = Bz = 𝐶)
2216, 21syl6bb 185 . . . . 5 (w = y → ([w / x]z = Bz = 𝐶))
2315, 22anbi12d 442 . . . 4 (w = y → ((w A [w / x]z = B) ↔ (y A z = 𝐶)))
2413, 14, 23cbvopab1 3821 . . 3 {⟨w, z⟩ ∣ (w A [w / x]z = B)} = {⟨y, z⟩ ∣ (y A z = 𝐶)}
258, 24eqtri 2057 . 2 {⟨x, z⟩ ∣ (x A z = B)} = {⟨y, z⟩ ∣ (y A z = 𝐶)}
26 df-mpt 3811 . 2 (x AB) = {⟨x, z⟩ ∣ (x A z = B)}
27 df-mpt 3811 . 2 (y A𝐶) = {⟨y, z⟩ ∣ (y A z = 𝐶)}
2825, 26, 273eqtr4i 2067 1 (x AB) = (y A𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1242   wcel 1390  [wsb 1642  wnfc 2162  {copab 3808  cmpt 3809
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-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  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-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-mpt 3811
This theorem is referenced by:  cbvmptv  3843  dffn5imf  5171  fvmpts  5193  fvmpt2  5197  mptfvex  5199  fmptcof  5274  fmptcos  5275  fliftfuns  5381  offval2  5668  qliftfuns  6126
  Copyright terms: Public domain W3C validator