New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 2347 | . . . . . 6 | |
2 | 1 | biimpi 186 | . . . . 5 |
3 | 2 | 19.21bi 1758 | . . . 4 |
4 | 3 | bibi1d 310 | . . 3 |
5 | 4 | albidv 1625 | . 2 |
6 | dfcleq 2347 | . 2 | |
7 | dfcleq 2347 | . 2 | |
8 | 5, 6, 7 | 3bitr4g 279 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 176 wal 1540 wceq 1642 wcel 1710 |
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 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-cleq 2346 |
This theorem is referenced by: eqeq1i 2360 eqeq1d 2361 eqeq2 2362 eqeq12 2365 eqtr 2370 eqsb3lem 2453 clelab 2473 neeq1 2524 pm13.18 2588 issetf 2864 sbhypf 2904 vtoclgft 2905 eqvincf 2967 pm13.183 2979 eueq 3008 mob 3018 euind 3023 reu6 3025 reu7 3031 reuind 3039 eqsbc3 3085 csbhypf 3171 uniiunlem 3353 snjust 3740 elprg 3750 elsncg 3755 sneqrg 3874 intab 3956 uniintsn 3963 dfiin2g 4000 pwadjoin 4119 preqr2g 4126 preq12bg 4128 el1c 4139 elxpk 4196 opkelopkabg 4245 opkelins2kg 4251 opkelins3kg 4252 opkelsikg 4264 sikss1c1c 4267 opkelidkg 4274 eladdc 4398 0nelsuc 4400 nnc0suc 4412 nndisjeq 4429 opklefing 4448 opkltfing 4449 leltfintr 4458 lefinlteq 4463 ltfintri 4466 tfineq 4488 tfin11 4493 0ceven 4505 evennn 4506 oddnn 4507 evennnul 4508 oddnnul 4509 sucevenodd 4510 sucoddeven 4511 evenodddisjlem1 4515 evenodddisj 4516 eventfin 4517 oddtfin 4518 nnadjoin 4520 nnadjoinpw 4521 tfinnn 4534 vfinncvntsp 4549 vfinspsslem1 4550 vfinspss 4551 dfphi2 4569 phi11lem1 4595 0cnelphi 4597 proj1op 4600 proj2op 4601 copsexg 4607 phialllem1 4616 elopab 4696 br1stg 4730 brsi 4761 elxpi 4800 opbrop 4841 br1st 4858 br2nd 4859 brswap2 4860 ideqg 4868 ideqg2 4869 funcnvuni 5161 fun11iun 5305 dffn5 5363 fvelrnb 5365 fvopab4t 5385 fvopab4g 5388 eqfnfv 5392 fnasrn 5417 foelrn 5425 foco2 5426 abrexco 5463 funiunfv 5467 dff13f 5472 f1fveq 5473 f1oiso 5499 brswap 5509 funsi 5520 oprabid 5550 eloprabga 5578 ov3 5599 ov6g 5600 ovelrn 5608 caovcan 5628 brsnsi 5773 brtxp 5783 op1st2nd 5790 fnpprod 5843 extd 5923 antid 5929 elqsg 5976 qsdisj 5995 ncseqnc 6128 ncspw1eu 6159 eqtc 6161 nc0le1 6216 taddc 6229 letc 6231 ce0t 6232 ce0lenc1 6239 muc0or 6252 csucex 6259 brcsuc 6260 addccan2nclem1 6263 addccan2nclem2 6264 nncdiv3 6277 nnc3n3p1 6278 spaccl 6286 spacind 6287 nchoicelem3 6291 nchoicelem12 6300 nchoicelem16 6304 frecsuc 6322 scancan 6331 |
Copyright terms: Public domain | W3C validator |