New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqeq1i | GIF version |
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq1i.1 | ⊢ A = B |
Ref | Expression |
---|---|
eqeq1i | ⊢ (A = C ↔ B = C) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1i.1 | . 2 ⊢ A = B | |
2 | eqeq1 2359 | . 2 ⊢ (A = B → (A = C ↔ B = C)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (A = C ↔ B = C) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 = wceq 1642 |
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: ssequn2 3436 dfss1 3460 dfss4 3489 disjr 3592 undisj1 3602 undisj2 3603 undif 3630 uneqdifeq 3638 reusn 3793 rabsneu 3795 eusn 3796 uniintsn 3963 dfiota4 4372 dfaddc2 4381 addccom 4406 addcass 4415 nndisjeq 4429 vfin1cltv 4547 phidisjnn 4615 opeqexb 4620 dmopab3 4917 dm0rn0 4921 ssdmres 4987 resabs1 4992 imadisj 5015 intirr 5029 dminxp 5061 funun 5146 fncnv 5158 dff1o4 5294 fvun2 5380 fvco2 5382 fvopab3ig 5387 fvpr2 5450 fnopovb 5557 ov 5595 ovigg 5596 ovg 5601 oprssdm 5612 brcupg 5814 braddcfn 5826 fnsex 5832 brcrossg 5848 brpw1fn 5854 brfullfung 5865 brfullfunop 5867 dfnnc3 5885 map0 6025 eqtc 6161 brtcfn 6246 nnc3n3p1 6278 nnc3n3p2 6279 nchoicelem14 6302 fnfreclem2 6318 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |