![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq1 | Unicode version |
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2034 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 113 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.21bi 1450 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bibi1d 222 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | albidv 1705 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | dfcleq 2034 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | dfcleq 2034 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | 3bitr4g 212 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqeq1i 2047 eqeq1d 2048 eqeq2 2049 eqeq12 2052 eqtr 2057 eqsb3lem 2140 clelab 2162 neeq1 2218 pm13.18 2286 issetf 2562 sbhypf 2603 vtoclgft 2604 eqvincf 2669 pm13.183 2681 eueq 2712 mob 2723 euind 2728 reuind 2744 eqsbc3 2802 csbhypf 2885 uniiunlem 3028 snjust 3380 elsng 3390 elprg 3395 rabrsndc 3438 sneqrg 3533 preq12bg 3544 intab 3644 dfiin2g 3690 opthg 3975 copsexg 3981 euotd 3991 elopab 3995 snnex 4181 uniuni 4183 eusv1 4184 reusv3 4192 ordtriexmid 4247 onsucelsucexmidlem1 4253 onsucelsucexmid 4255 regexmidlemm 4257 regexmidlem1 4258 reg2exmidlema 4259 wetriext 4301 nn0suc 4327 nndceq0 4339 0elnn 4340 elxpi 4361 opbrop 4419 relop 4486 ideqg 4487 elrnmpt 4583 elrnmpt1 4585 elrnmptg 4586 cnveqb 4776 relcoi1 4849 funopg 4934 funcnvuni 4968 fun11iun 5147 fvelrnb 5221 fvmptg 5248 fndmin 5274 eldmrexrn 5308 foelrn 5317 foco2 5318 fmptco 5330 elabrex 5397 abrexco 5398 f1veqaeq 5408 f1oiso 5465 eusvobj2 5498 acexmidlema 5503 acexmidlemb 5504 acexmidlem2 5509 acexmidlemv 5510 oprabid 5537 mpt2fun 5603 elrnmpt2g 5613 elrnmpt2 5614 ralrnmpt2 5615 rexrnmpt2 5616 ovi3 5637 ov6g 5638 ovelrn 5649 caovcang 5662 caovcan 5665 eloprabi 5822 dftpos4 5878 elqsg 6156 qsel 6183 brecop 6196 eroveu 6197 erovlem 6198 th3qlem1 6208 th3q 6211 2dom 6285 fundmen 6286 nneneq 6320 indpi 6440 nqtri3or 6494 enq0sym 6530 enq0ref 6531 enq0tr 6532 enq0breq 6534 addnq0mo 6545 mulnq0mo 6546 mulnnnq0 6548 genipv 6607 genpelvl 6610 genpelvu 6611 addsrmo 6828 mulsrmo 6829 aptisr 6863 ltresr 6915 axcnre 6955 axpre-apti 6959 apreap 7578 apreim 7594 creur 7911 creui 7912 nn1m1nn 7932 nn1gt1 7947 elz 8247 nn0ind-raph 8355 nltpnft 8730 xnegeq 8740 flqeqceilz 9160 expival 9257 shftfvalg 9419 shftfval 9422 bj-nn0suc0 10075 bj-inf2vnlem1 10095 bj-inf2vnlem2 10096 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |