![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ideq | Structured version Visualization version GIF version |
Description: For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
ideq.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
ideq | ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ideq.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | ideqg 5615 | . 2 ⊢ (𝐵 ∈ V → (𝐴 I 𝐵 ↔ 𝐴 = 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 I 𝐵 ↔ 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1525 ∈ wcel 2083 Vcvv 3440 class class class wbr 4968 I cid 5354 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pr 5228 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-br 4969 df-opab 5031 df-id 5355 df-xp 5456 df-rel 5457 |
This theorem is referenced by: dmi 5684 resieq 5752 iss 5791 elidinxp 5799 restidsing 5807 imai 5825 intasym 5858 asymref 5859 intirr 5861 poirr2 5867 cnvi 5883 xpdifid 5908 coi1 5997 dffv2 6630 isof1oidb 6947 idssen 8409 dflt2 12395 relexpindlem 14260 opsrtoslem2 19956 hausdiag 21941 hauseqlcld 21942 metustid 22851 ltgov 26069 ex-id 27901 dfso2 32600 dfpo2 32601 idsset 32962 dfon3 32964 elfix 32975 dffix2 32977 sscoid 32985 dffun10 32986 elfuns 32987 brsingle 32989 brapply 33010 brsuccf 33013 dfrdg4 33023 iss2 35154 undmrnresiss 39470 dffrege99 39814 ipo0 40341 ifr0 40342 fourierdlem42 41998 |
Copyright terms: Public domain | W3C validator |