![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleq2 | Unicode version |
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleq2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2031 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpi 113 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 19.21bi 1447 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | anbi2d 437 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | exbidv 1703 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | df-clel 2033 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | df-clel 2033 |
. 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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 |
This theorem is referenced by: eleq12 2099 eleq2i 2101 eleq2d 2104 nelneq2 2136 clelsb4 2140 dvelimdc 2194 nelne1 2289 neleq2 2296 raleqf 2495 rexeqf 2496 reueq1f 2497 rmoeq1f 2498 rabeqf 2544 clel3g 2672 clel4 2674 sbcel2gv 2816 sbnfc2 2900 difeq2 3050 uneq1 3084 ineq1 3125 n0i 3223 disjel 3268 exsnrex 3404 sneqr 3522 preqr1g 3528 preqr1 3530 preq12b 3532 prel12 3533 elunii 3576 eluniab 3583 ssuni 3593 elinti 3615 elintab 3617 intss1 3621 intmin 3626 intab 3635 iineq2 3665 dfiin2g 3681 breq 3757 axsep2 3867 zfauscl 3868 inuni 3900 rext 3942 intid 3951 mss 3953 opth1 3964 opeqex 3977 limeq 4080 nsuceq0g 4121 suctr 4124 snnex 4147 uniuni 4149 iunpw 4177 ordtriexmidlem 4208 ordtriexmidlem2 4209 ordtriexmid 4210 ordtri2orexmid 4211 onsucelsucexmidlem 4214 onsucelsucexmid 4215 ordsucunielexmid 4216 regexmidlem1 4218 regexmid 4219 elirr 4224 en2lp 4232 suc11g 4235 dtruex 4237 ordsoexmid 4240 nlimsucg 4242 onpsssuc 4247 peano5 4264 limom 4279 0elnn 4283 nn0eln0 4284 nnregexmid 4285 xpeq1 4302 xpeq2 4303 opthprc 4334 xp11m 4702 funopg 4877 dffo4 5258 elunirn 5348 f1oiso 5408 eusvobj2 5441 acexmidlema 5446 acexmidlemb 5447 acexmidlemab 5449 acexmidlem2 5452 mpt2eq123 5506 unielxp 5742 cnvf1o 5788 smoel 5856 tfr0 5878 nnsucelsuc 6009 nntri3or 6011 nntri2 6012 nntri3 6014 nndceq 6015 nnmordi 6025 nnaordex 6036 elqsn0m 6110 qsel 6119 elni2 6298 addnidpig 6320 elinp 6457 pitonn 6744 peano5nni 7698 1nn 7706 peano2nn 7707 dfuzi 8124 uz11 8271 elfzonlteqm1 8836 frec2uzltd 8870 bdsep2 9341 bdzfauscl 9345 bj-indeq 9388 bj-nn0suc0 9410 bj-nnelirr 9413 bj-peano4 9415 bj-inf2vnlem2 9431 bj-nn0sucALT 9438 bj-findis 9439 |
Copyright terms: Public domain | W3C validator |