New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eqeltri | Unicode version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeltr.1 | |
eqeltr.2 |
Ref | Expression |
---|---|
eqeltri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltr.2 | . 2 | |
2 | eqeltr.1 | . . 3 | |
3 | 2 | eleq1i 2416 | . 2 |
4 | 1, 3 | mpbir 200 | 1 |
Colors of variables: wff setvar class |
Syntax hints: 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-an 360 df-ex 1542 df-cleq 2346 df-clel 2349 |
This theorem is referenced by: eqeltrri 2424 3eltr4i 2432 intab 3956 prex 4112 opkex 4113 idkex 4314 setswithex 4322 0cex 4392 nncex 4396 finex 4397 1cnnc 4408 preaddccan2lem1 4454 ltfinex 4464 ncfinex 4472 tfinex 4485 evenfinex 4503 oddfinex 4504 spfinex 4537 nulnnn 4556 phialllem1 4616 1stex 4739 swapex 4742 ssetex 4744 xpvv 4843 2ndex 5112 fvex 5339 idex 5504 1stfo 5505 2ndfo 5506 swapf1o 5511 ovex 5551 ins4ex 5799 si3ex 5806 cupex 5816 composeex 5820 disjex 5823 addcfnex 5824 funsex 5828 fnsex 5832 crossex 5850 pw1fnex 5852 domfnex 5870 ranfnex 5871 clos1ex 5876 clos1induct 5880 clos1basesuc 5882 transex 5910 refex 5911 antisymex 5912 connexex 5913 foundex 5914 extex 5915 symex 5916 partialex 5917 strictex 5918 weex 5919 erex 5920 enex 6031 enmap2lem1 6063 enmap1lem1 6069 enprmaplem1 6076 enprmaplem4 6079 ncsex 6111 lecex 6115 ltcex 6116 ncex 6117 muccl 6132 mucex 6133 0cnc 6138 nnnc 6146 tcex 6157 tcdi 6164 ceex 6174 ce0addcnnul 6179 ce0nn 6180 ceclb 6183 ce2 6192 sbthlem1 6203 tcfnex 6244 csucex 6259 nncdiv3lem2 6276 |
Copyright terms: Public domain | W3C validator |