New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > equid | GIF version |
Description: Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 9-Dec-2017.) |
Ref | Expression |
---|---|
equid | ⊢ x = x |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a9ev 1656 | . 2 ⊢ ∃y y = x | |
2 | ax-8 1675 | . . . 4 ⊢ (y = x → (y = x → x = x)) | |
3 | 2 | pm2.43i 43 | . . 3 ⊢ (y = x → x = x) |
4 | 3 | eximi 1576 | . 2 ⊢ (∃y y = x → ∃y x = x) |
5 | ax17e 1618 | . 2 ⊢ (∃y x = x → x = x) | |
6 | 1, 4, 5 | mp2b 9 | 1 ⊢ x = x |
Colors of variables: wff setvar class |
Syntax hints: ∃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 |
This theorem depends on definitions: df-bi 177 df-ex 1542 |
This theorem is referenced by: nfequid 1678 equcomi 1679 stdpc6 1687 19.2OLD 1700 ax9dgen 1716 ax12dgen1 1725 ax12dgen3 1727 sbid 1922 equveli 1988 ax11eq 2193 exists1 2293 vjust 2860 sbc8g 3053 rab0 3571 dfid3 4768 fvi 5442 2ndfo 5506 |
Copyright terms: Public domain | W3C validator |