New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  dvelimv GIF version

Theorem dvelimv 1939
 Description: Similar to dvelim 2016 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.)
Hypothesis
Ref Expression
dvelimv.1 (z = y → (φψ))
Assertion
Ref Expression
dvelimv x x = y → (ψxψ))
Distinct variable groups:   x,z   y,z   ψ,z   φ,x
Allowed substitution hints:   φ(y,z)   ψ(x,y)

Proof of Theorem dvelimv
StepHypRef Expression
1 ax-17 1616 . . . . . 6 (ψzψ)
21a1d 22 . . . . . 6 (ψ → (z = yzψ))
31, 2alrimih 1565 . . . . 5 (ψz(z = yzψ))
4 sp 1747 . . . . . . . 8 (zψψ)
5 dvelimv.1 . . . . . . . 8 (z = y → (φψ))
64, 5syl5ibr 212 . . . . . . 7 (z = y → (zψφ))
76a2i 12 . . . . . 6 ((z = yzψ) → (z = yφ))
87alimi 1559 . . . . 5 (z(z = yzψ) → z(z = yφ))
93, 8syl 15 . . . 4 (ψz(z = yφ))
10 ax10lem3 1938 . . . . . . . 8 (z z = xx x = z)
1110con3i 127 . . . . . . 7 x x = z → ¬ z z = x)
12 hbn1 1730 . . . . . . . 8 z z = xz ¬ z z = x)
13 ax10lem3 1938 . . . . . . . . 9 (x x = zz z = x)
1413con3i 127 . . . . . . . 8 z z = x → ¬ x x = z)
1512, 14alrimih 1565 . . . . . . 7 z z = xz ¬ x x = z)
1611, 15syl 15 . . . . . 6 x x = zz ¬ x x = z)
17 ax-17 1616 . . . . . 6 x x = yz ¬ x x = y)
1816, 17hban 1828 . . . . 5 ((¬ x x = z ¬ x x = y) → zx x = z ¬ x x = y))
19 hbn1 1730 . . . . . . 7 x x = zx ¬ x x = z)
20 hbn1 1730 . . . . . . 7 x x = yx ¬ x x = y)
2119, 20hban 1828 . . . . . 6 ((¬ x x = z ¬ x x = y) → xx x = z ¬ x x = y))
22 ax12o 1934 . . . . . . 7 x x = z → (¬ x x = y → (z = yx z = y)))
2322imp 418 . . . . . 6 ((¬ x x = z ¬ x x = y) → (z = yx z = y))
24 a17d 1617 . . . . . 6 ((¬ x x = z ¬ x x = y) → (φxφ))
2521, 23, 24hbimd 1815 . . . . 5 ((¬ x x = z ¬ x x = y) → ((z = yφ) → x(z = yφ)))
2618, 25hbald 1740 . . . 4 ((¬ x x = z ¬ x x = y) → (z(z = yφ) → xz(z = yφ)))
275biimpd 198 . . . . . . . . 9 (z = y → (φψ))
2827a2i 12 . . . . . . . 8 ((z = yφ) → (z = yψ))
2928alimi 1559 . . . . . . 7 (z(z = yφ) → z(z = yψ))
30 ax9v 1655 . . . . . . . 8 ¬ z ¬ z = y
31 con3 126 . . . . . . . . 9 ((z = yψ) → (¬ ψ → ¬ z = y))
3231al2imi 1561 . . . . . . . 8 (z(z = yψ) → (z ¬ ψz ¬ z = y))
3330, 32mtoi 169 . . . . . . 7 (z(z = yψ) → ¬ z ¬ ψ)
3429, 33syl 15 . . . . . 6 (z(z = yφ) → ¬ z ¬ ψ)
35 ax-17 1616 . . . . . 6 ψz ¬ ψ)
3634, 35nsyl2 119 . . . . 5 (z(z = yφ) → ψ)
3736alimi 1559 . . . 4 (xz(z = yφ) → xψ)
389, 26, 37syl56 30 . . 3 ((¬ x x = z ¬ x x = y) → (ψxψ))
3938expcom 424 . 2 x x = y → (¬ x x = z → (ψxψ)))
40 sp 1747 . . . 4 (x x = zx = z)
41 ax-11 1746 . . . 4 (x = z → (zψx(x = zψ)))
4240, 1, 41syl2im 34 . . 3 (x x = z → (ψx(x = zψ)))
43 pm2.27 35 . . . 4 (x = z → ((x = zψ) → ψ))
4443al2imi 1561 . . 3 (x x = z → (x(x = zψ) → xψ))
4542, 44syld 40 . 2 (x x = z → (ψxψ))
4639, 45pm2.61d2 152 1 x x = y → (ψxψ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545 This theorem is referenced by:  dveeq2  1940  ax10lem4  1941  dveeq1  2018  dveel1  2019  dveel2  2020  rgen2a  2680
 Copyright terms: Public domain W3C validator