New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > equcom | GIF version |
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.) |
Ref | Expression |
---|---|
equcom | ⊢ (x = y ↔ y = x) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1679 | . 2 ⊢ (x = y → y = x) | |
2 | equcomi 1679 | . 2 ⊢ (y = x → x = y) | |
3 | 1, 2 | impbii 180 | 1 ⊢ (x = y ↔ y = x) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 |
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: equequ2 1686 ax12olem6 1932 eu1 2225 2eu6 2289 reu8 3032 iunid 4021 unipw1 4325 addcid1 4405 evenodddisjlem1 4515 dfphi2 4569 proj1op 4600 proj2op 4601 copsexg 4607 phidisjnn 4615 dfid3 4768 opeliunxp 4820 dmi 4919 opabresid 5003 intirr 5029 cnvi 5032 coi1 5094 trtxp 5781 oqelins4 5794 fvfullfunlem1 5861 extex 5915 enpw1lem1 6061 el2c 6191 addccan2nclem1 6263 fnfreclem1 6317 scancan 6331 |
Copyright terms: Public domain | W3C validator |