Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfsb4t Unicode version

Theorem nfsb4t 2127
 Description: A variable not free remains so after substitution with a distinct variable (closed form of nfsb4 2128). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.)
Assertion
Ref Expression
nfsb4t

Proof of Theorem nfsb4t
StepHypRef Expression
1 sbequ12 1940 . . . . . . . . 9
21sps 1766 . . . . . . . 8
32drnf2 2027 . . . . . . 7
43biimpcd 216 . . . . . 6
54sps 1766 . . . . 5
65a1dd 44 . . . 4
7 nfa1 1802 . . . . . . . 8
8 nfnae 2008 . . . . . . . . 9
9 nfnae 2008 . . . . . . . . 9
108, 9nfan 1842 . . . . . . . 8
117, 10nfan 1842 . . . . . . 7
12 nfeqf 2014 . . . . . . . . 9
1312adantl 453 . . . . . . . 8
14 sp 1759 . . . . . . . . 9
1514adantr 452 . . . . . . . 8
1613, 15nfimd 1823 . . . . . . 7
1711, 16nfald 1867 . . . . . 6
1817ex 424 . . . . 5
19 nfnae 2008 . . . . . . 7
20 sb4b 2101 . . . . . . 7
2119, 20nfbidf 1786 . . . . . 6
2221imbi2d 308 . . . . 5
2318, 22syl5ibrcom 214 . . . 4
246, 23pm2.61d 152 . . 3
2524exp3a 426 . 2
26 nfsb2 2105 . . 3
27 drsb1 2069 . . . 4
2827drnf2 2027 . . 3
2926, 28syl5ib 211 . 2
3025, 29pm2.61d2 154 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359  wal 1546  wnf 1550  wsb 1655 This theorem is referenced by:  nfsb4  2128  dvelimdf  2129  nfsbd  2158 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946 This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656
 Copyright terms: Public domain W3C validator