| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eleqtrrid | Structured version Visualization version GIF version | ||
| Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
| Ref | Expression |
|---|---|
| eleqtrrid.1 | ⊢ 𝐴 ∈ 𝐵 |
| eleqtrrid.2 | ⊢ (𝜑 → 𝐶 = 𝐵) |
| Ref | Expression |
|---|---|
| eleqtrrid | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleqtrrid.1 | . 2 ⊢ 𝐴 ∈ 𝐵 | |
| 2 | eleqtrrid.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐵) | |
| 3 | 2 | eqcomd 2743 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
| 4 | 1, 3 | eleqtrid 2847 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: rabsnt 4731 onnev 6511 opabiota 6991 canth 7385 onnseq 8384 tfrlem16 8433 oen0 8624 nnawordex 8675 inf0 9661 cantnflt 9712 cnfcom2 9742 cnfcom3lem 9743 cnfcom3 9744 r1ordg 9818 r1val1 9826 rankr1id 9902 acacni 10181 dfacacn 10182 dfac13 10183 ttukeylem5 10553 ttukeylem6 10554 gch2 10715 gch3 10716 gchac 10721 gchina 10739 swrds1 14704 wrdl3s3 15001 sadcp1 16492 lcmfunsnlem2 16677 fnpr2ob 17603 idfucl 17926 gsumval2 18699 gsumz 18849 frmdmnd 18872 frmd0 18873 efginvrel2 19745 efgcpbl2 19775 pgpfaclem1 20101 lbsexg 21166 zringndrg 21479 frlmlbs 21817 mat0dimscm 22475 mat0scmat 22544 m2detleiblem5 22631 m2detleiblem6 22632 m2detleiblem3 22635 m2detleiblem4 22636 d0mat2pmat 22744 chpmat0d 22840 dfac14 23626 acufl 23925 cnextfvval 24073 cnextcn 24075 minveclem3b 25462 minveclem4a 25464 ovollb2 25524 ovolunlem1a 25531 ovolunlem1 25532 ovoliunlem1 25537 ovoliun2 25541 ioombl1lem4 25596 uniioombllem1 25616 uniioombllem2 25618 uniioombllem6 25623 itg2monolem1 25785 itg2mono 25788 itg2cnlem1 25796 xrlimcnp 27011 efrlim 27012 efrlimOLD 27013 eengbas 28996 ebtwntg 28997 ecgrtg 28998 elntg 28999 wlkl1loop 29656 elwwlks2ons3im 29974 upgr3v3e3cycl 30199 upgr4cycl4dv4e 30204 2clwwlk2clwwlk 30369 ex-br 30450 trsp2cyc 33143 cyc3evpm 33170 ply1dg1rtn0 33605 lvecdim0 33657 extdg1id 33716 irngss 33737 rge0scvg 33948 repr0 34626 hgt750lemg 34669 mrsub0 35521 elmrsubrn 35525 topjoin 36366 finorwe 37383 pclfinN 39902 aomclem1 43066 dfac21 43078 naddgeoa 43407 clsk1indlem1 44058 mnurndlem1 44300 fourierdlem102 46223 fourierdlem114 46235 cycl3grtri 47914 lincval0 48332 lcoel0 48345 prsthinc 49111 |
| Copyright terms: Public domain | W3C validator |