Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeltri | GIF 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 2144 | . 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) |
4 | 1, 3 | mpbir 144 | 1 ⊢ 𝐴 ∈ 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1284 ∈ wcel 1433 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 ax-ext 2063 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 df-clel 2077 |
This theorem is referenced by: eqeltrri 2152 3eltr4i 2160 intab 3665 inex2 3913 pwex 3953 ord3ex 3961 uniopel 4011 onsucelsucexmid 4273 elvvuni 4422 isarep2 5006 acexmidlemcase 5527 abrexex2 5771 oprabex 5775 oprabrexex2 5777 rdg0 5997 frecex 6004 1on 6031 2on 6032 3on 6034 4on 6035 1onn 6116 2onn 6117 3onn 6118 4onn 6119 fnfi 6388 nqex 6553 nq0ex 6630 1pr 6744 ltexprlempr 6798 recexprlempr 6822 cauappcvgprlemcl 6843 caucvgprlemcl 6866 caucvgprprlemcl 6894 addvalex 7012 peano1nnnn 7020 peano2nnnn 7021 axcnex 7027 ax1cn 7029 ax1re 7030 inelr 7684 cju 8038 2re 8109 3re 8113 4re 8116 5re 8118 6re 8120 7re 8122 8re 8124 9re 8126 2nn 8193 3nn 8194 4nn 8195 5nn 8196 6nn 8197 7nn 8198 8nn 8199 9nn 8200 nn0ex 8294 nneoor 8449 zeo 8452 deccl 8491 decnncl 8496 numnncl2 8499 decnncl2 8500 numsucc 8516 numma2c 8522 numadd 8523 numaddc 8524 nummul1c 8525 nummul2c 8526 pnfxr 8846 mnfxr 8848 xnegcl 8899 xrex 8910 ioof 8994 iseqex 9433 m1expcl2 9498 faccl 9662 facwordi 9667 faclbnd2 9669 bccl 9694 crre 9744 remim 9747 absval 9887 climle 10172 climcvg1nlem 10186 nn0o 10307 bdinex2 10691 bj-inex 10698 |
Copyright terms: Public domain | W3C validator |