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

Theorem eujustALT 2286
 Description: A soundness justification theorem for df-eu 2287, 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 2074. (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 1699 . . . . . 6
21bibi2d 311 . . . . 5
32albidv 1636 . . . 4
43sps 1771 . . 3
54drex1 2060 . 2
6 hbnae 2044 . . . . . 6
7 hbnae 2044 . . . . . 6
86, 7alrimih 1575 . . . . 5
9 ax-17 1627 . . . . . . . 8
10 equequ2 1699 . . . . . . . . . . 11
1110bibi2d 311 . . . . . . . . . 10
1211albidv 1636 . . . . . . . . 9
1312notbid 287 . . . . . . . 8
149, 13dvelim 2074 . . . . . . 7
1514naecoms 2038 . . . . . 6
16 ax-17 1627 . . . . . . 7
17 equequ2 1699 . . . . . . . . . 10
1817bibi2d 311 . . . . . . . . 9
1918albidv 1636 . . . . . . . 8
2019notbid 287 . . . . . . 7
2116, 20dvelim 2074 . . . . . 6
223notbid 287 . . . . . . 7
2322a1i 11 . . . . . 6
2415, 21, 23cbv2h 1980 . . . . 5
258, 24syl 16 . . . 4
2625notbid 287 . . 3
27 df-ex 1552 . . 3
28 df-ex 1552 . . 3
2926, 27, 283bitr4g 281 . 2
305, 29pm2.61i 159 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178  wal 1550  wex 1551 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555
 Copyright terms: Public domain W3C validator