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

Theorem eujustALT 2207
 Description: A soundness justification theorem for df-eu 2208, showing that the definition is equivalent to itself with its dummy variable renamed. Note that and needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 2016. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
eujustALT
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem eujustALT
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 equequ2 1686 . . . . . 6
21bibi2d 309 . . . . 5
32albidv 1625 . . . 4
43sps 1754 . . 3
54drex1 1967 . 2
6 hbnae 1955 . . . . . 6
7 hbnae 1955 . . . . . 6
86, 7alrimih 1565 . . . . 5
9 ax-17 1616 . . . . . . . 8
10 equequ2 1686 . . . . . . . . . . 11
1110bibi2d 309 . . . . . . . . . 10
1211albidv 1625 . . . . . . . . 9
1312notbid 285 . . . . . . . 8
149, 13dvelim 2016 . . . . . . 7
1514naecoms 1948 . . . . . 6
16 ax-17 1616 . . . . . . 7
17 equequ2 1686 . . . . . . . . . 10
1817bibi2d 309 . . . . . . . . 9
1918albidv 1625 . . . . . . . 8
2019notbid 285 . . . . . . 7
2116, 20dvelim 2016 . . . . . 6
223notbid 285 . . . . . . 7
2322a1i 10 . . . . . 6
2415, 21, 23cbv2h 1980 . . . . 5
258, 24syl 15 . . . 4
2625notbid 285 . . 3
27 df-ex 1542 . . 3
28 df-ex 1542 . . 3
2926, 27, 283bitr4g 279 . 2
305, 29pm2.61i 156 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 176  wal 1540  wex 1541 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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: (None)
 Copyright terms: Public domain W3C validator