| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqeltrrdi | Structured version Visualization version GIF version | ||
| Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
| Ref | Expression |
|---|---|
| eqeltrrdi.1 | ⊢ (𝜑 → 𝐵 = 𝐴) |
| eqeltrrdi.2 | ⊢ 𝐵 ∈ 𝐶 |
| Ref | Expression |
|---|---|
| eqeltrrdi | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeltrrdi.1 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐴) | |
| 2 | 1 | eqcomd 2743 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
| 3 | eqeltrrdi.2 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
| 4 | 2, 3 | eqeltrdi 2849 | 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: axrep6g 5290 snexg 5435 wemoiso2 7999 releldm2 8068 mapprc 8870 mapfoss 8892 ixpprc 8959 bren 8995 brdomg 8997 brdomgOLD 8998 domssex 9178 mapen 9181 ssenen 9191 imafiOLD 9354 fodomfib 9369 fodomfibOLD 9371 fi0 9460 dffi3 9471 brwdom 9607 brwdomn0 9609 unxpwdom2 9628 ixpiunwdom 9630 tcmin 9781 rankonid 9869 rankr1id 9902 cardf2 9983 cardid2 9993 carduni 10021 fseqen 10067 acndom 10091 acndom2 10094 alephnbtwn 10111 cardcf 10292 cfeq0 10296 cflim2 10303 coftr 10313 infpssr 10348 hsmexlem5 10470 axdc3lem4 10493 fodomb 10566 ondomon 10603 gruina 10858 ioof 13487 hashbc 14492 trclun 15053 zsum 15754 fsum 15756 fprod 15977 eqgen 19199 symgfisg 19486 dvdsr 20362 asplss 21894 aspsubrg 21896 psrval 21935 clsf 23056 restco 23172 subbascn 23262 is2ndc 23454 ptbasin2 23586 ptbas 23587 indishmph 23806 ufldom 23970 cnextfres1 24076 ussid 24269 icopnfcld 24788 cnrehmeo 24984 cnrehmeoOLD 24985 csscld 25283 clsocv 25284 itg2gt0 25795 dvmptadd 25998 dvmptmul 25999 dvmptco 26010 logcn 26689 selberglem1 27589 noseq0 28296 hmopidmchi 32170 evl1deg2 33602 sigagensiga 34142 dya2iocbrsiga 34277 dya2icobrsiga 34278 logdivsqrle 34665 fnessref 36358 bj-snexg 37035 bj-unexg 37039 unirep 37721 indexdom 37741 dicfnN 41185 pwslnmlem0 43103 mendval 43191 icof 45224 dvsubf 45929 dvdivf 45937 itgsinexplem1 45969 stirlinglem7 46095 fourierdlem73 46194 fouriersw 46246 ovolval4lem1 46664 i0oii 48817 io1ii 48818 |
| Copyright terms: Public domain | W3C validator |