HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Inference from equality to equivalence of equalities. |
| Ref | Expression |
|---|---|
| eqeq1i.1 |
    |
| Ref | Expression |
|---|---|
| eqeq1i |
    |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1i.1 |
. 2
| |
| 2 | eqeq1 1473 |
. 2
 | |
| 3 | 1, 2 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wb 146
wceq 953 |
| This theorem is referenced by: eqeq12i 1480 ssequn2 2193 sseqin2 2219 dfss4 2232 disj 2301 undisj1 2310 undisj2 2311 undif 2333 iin0 2730 opeqsn 2791 reuuni1 2872 reusn 2882 dfepfr 2922 epfrc 2923 unisuc 3036 dmopab3 3311 dm0rn0 3319 dmxp 3321 ssdmres 3365 imadisj 3406 args 3412 dffr3 3415 dminxp 3469 dfrel3 3475 fncnv 3547 f1o4 3681 f1ocnv 3686 fvopab3ig 3763 fopab2 3808 tz7.44-2 3914 tz7.49c 3945 oprabval 4008 oprabvalig 4009 oprssdm 4027 map0 4328 pw2en 4426 mapunen 4482 zfreg2 4569 sucprcreg 4572 inf3lem2 4586 rankeq0 4668 rankxpsuc 4687 scott0s 4691 cplem1 4692 zorn2lem7 4766 recexsr 5188 map2psrpr 5192 supsrlem2 5198 subadd 5343 subadd2 5345 subsub23 5346 neg11 5378 negcon1 5379 renegcl 5388 lesubadd 5569 divmul 5674 xrsupss 6025 xrinfmss 6026 elznn0 6096 zltp1let 6128 sq00 6546 sqeqor 6578 sqr2irrlem1 6654 crulem 6666 negreb 6730 abs00 6777 cvgcmpub 7121 geoser 7169 ivth2OLD 7234 eirrlem5 7334 elcls 7646 islp2 7688 qdensere 7691 lpbl 7819 bcthlem9 7941 nmlno0lem 8385 logeftb 8686 logeftbOLD 8706 hvsubeq0 8851 hvsubadd 8854 pjoc2 9186 pjoml3 9446 cmbr3 9460 nonbool 9513 pjss2 9542 hosubeq0 9669 dmadjrnb 9747 nmlnop0ALT 9835 nmcopexlem1 9866 nmcfnexlem1 9895 pj3lem1 10044 stm1r 10081 jplem2 10106 atoml2 10218 irredlem1 10225 cdj3lem3 10270 oprabvaligg 10341 efilcp 10445 efilcp2 10450 homib 10568 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-gen 960 ax-17 968 ax-4 970 ax-5o 972 ax-ext 1452 |
| This theorem depends on definitions: df-bi 147 df-an 225 df-cleq 1462 |