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

Theorem cbvreucsf 3064
 Description: A more general version of cbvreuv 2656 that has no distinct variable rextrictions. Changes bound variables using implicit substitution. (Contributed by Andrew Salmon, 13-Jul-2011.)
Hypotheses
Ref Expression
cbvralcsf.1 𝑦𝐴
cbvralcsf.2 𝑥𝐵
cbvralcsf.3 𝑦𝜑
cbvralcsf.4 𝑥𝜓
cbvralcsf.5 (𝑥 = 𝑦𝐴 = 𝐵)
cbvralcsf.6 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvreucsf (∃!𝑥𝐴 𝜑 ↔ ∃!𝑦𝐵 𝜓)

Proof of Theorem cbvreucsf
Dummy variables 𝑣 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1508 . . . 4 𝑧(𝑥𝐴𝜑)
2 nfcsb1v 3035 . . . . . 6 𝑥𝑧 / 𝑥𝐴
32nfcri 2275 . . . . 5 𝑥 𝑧𝑧 / 𝑥𝐴
4 nfs1v 1912 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1544 . . . 4 𝑥(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 id 19 . . . . . 6 (𝑥 = 𝑧𝑥 = 𝑧)
7 csbeq1a 3012 . . . . . 6 (𝑥 = 𝑧𝐴 = 𝑧 / 𝑥𝐴)
86, 7eleq12d 2210 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝑧 / 𝑥𝐴))
9 sbequ12 1744 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
108, 9anbi12d 464 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)))
111, 5, 10cbveu 2023 . . 3 (∃!𝑥(𝑥𝐴𝜑) ↔ ∃!𝑧(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑))
12 nfcv 2281 . . . . . . 7 𝑦𝑧
13 cbvralcsf.1 . . . . . . 7 𝑦𝐴
1412, 13nfcsb 3037 . . . . . 6 𝑦𝑧 / 𝑥𝐴
1514nfcri 2275 . . . . 5 𝑦 𝑧𝑧 / 𝑥𝐴
16 cbvralcsf.3 . . . . . 6 𝑦𝜑
1716nfsb 1919 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1815, 17nfan 1544 . . . 4 𝑦(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)
19 nfv 1508 . . . 4 𝑧(𝑦𝐵𝜓)
20 id 19 . . . . . 6 (𝑧 = 𝑦𝑧 = 𝑦)
21 csbeq1 3006 . . . . . . 7 (𝑧 = 𝑦𝑧 / 𝑥𝐴 = 𝑦 / 𝑥𝐴)
22 sbsbc 2913 . . . . . . . . 9 ([𝑦 / 𝑥]𝑣𝐴[𝑦 / 𝑥]𝑣𝐴)
2322abbii 2255 . . . . . . . 8 {𝑣 ∣ [𝑦 / 𝑥]𝑣𝐴} = {𝑣[𝑦 / 𝑥]𝑣𝐴}
24 cbvralcsf.2 . . . . . . . . . . . 12 𝑥𝐵
2524nfcri 2275 . . . . . . . . . . 11 𝑥 𝑣𝐵
26 cbvralcsf.5 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐴 = 𝐵)
2726eleq2d 2209 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑣𝐴𝑣𝐵))
2825, 27sbie 1764 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑣𝐴𝑣𝐵)
2928bicomi 131 . . . . . . . . 9 (𝑣𝐵 ↔ [𝑦 / 𝑥]𝑣𝐴)
3029abbi2i 2254 . . . . . . . 8 𝐵 = {𝑣 ∣ [𝑦 / 𝑥]𝑣𝐴}
31 df-csb 3004 . . . . . . . 8 𝑦 / 𝑥𝐴 = {𝑣[𝑦 / 𝑥]𝑣𝐴}
3223, 30, 313eqtr4ri 2171 . . . . . . 7 𝑦 / 𝑥𝐴 = 𝐵
3321, 32syl6eq 2188 . . . . . 6 (𝑧 = 𝑦𝑧 / 𝑥𝐴 = 𝐵)
3420, 33eleq12d 2210 . . . . 5 (𝑧 = 𝑦 → (𝑧𝑧 / 𝑥𝐴𝑦𝐵))
35 sbequ 1812 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
36 cbvralcsf.4 . . . . . . 7 𝑥𝜓
37 cbvralcsf.6 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
3836, 37sbie 1764 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
3935, 38syl6bb 195 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
4034, 39anbi12d 464 . . . 4 (𝑧 = 𝑦 → ((𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐵𝜓)))
4118, 19, 40cbveu 2023 . . 3 (∃!𝑧(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ ∃!𝑦(𝑦𝐵𝜓))
4211, 41bitri 183 . 2 (∃!𝑥(𝑥𝐴𝜑) ↔ ∃!𝑦(𝑦𝐵𝜓))
43 df-reu 2423 . 2 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑥(𝑥𝐴𝜑))
44 df-reu 2423 . 2 (∃!𝑦𝐵 𝜓 ↔ ∃!𝑦(𝑦𝐵𝜓))
4542, 43, 443bitr4i 211 1 (∃!𝑥𝐴 𝜑 ↔ ∃!𝑦𝐵 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331  Ⅎwnf 1436   ∈ wcel 1480  [wsb 1735  ∃!weu 1999  {cab 2125  Ⅎwnfc 2268  ∃!wreu 2418  [wsbc 2909  ⦋csb 3003 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-reu 2423  df-sbc 2910  df-csb 3004 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator