| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > risset | Structured version Visualization version GIF version | ||
| Description: Two ways to say "𝐴 belongs to 𝐵". (Contributed by NM, 22-Nov-1994.) |
| Ref | Expression |
|---|---|
| risset | ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exancom 1862 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 2 | df-rex 3061 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
| 3 | dfclel 2812 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 4 | 1, 2, 3 | 3bitr4ri 304 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1541 ∃wex 1780 ∈ wcel 2113 ∃wrex 3060 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-clel 2811 df-rex 3061 |
| This theorem is referenced by: nelb 3212 ceqsralv 3481 clel5 3619 reueq 3695 reuind 3711 0el 4315 reusv3 5350 elidinxp 6003 sucel 6393 fvmptt 6961 releldm2 7987 qsid 8718 ttrcltr 9625 zorng 10414 rereccl 11859 nndiv 12191 incexc2 15761 ruclem12 16166 chnfi 18557 conjnmzb 19182 pgpfac1lem2 20006 pgpfac1lem4 20009 mat1dimelbas 22415 mat1dimbas 22416 chmaidscmat 22792 unisngl 23471 fmid 23904 dcubic 26812 addsrid 27960 addsprop 27972 negsprop 28031 mulsrid 28109 mulsprop 28126 onsfi 28352 fusgrn0degnn0 29573 chscllem2 31713 disjunsn 32669 grplsm0l 33484 ballotlemsima 34673 dfon2lem8 35982 brimg 36129 dfrecs2 36144 altopelaltxp 36170 prtlem9 39124 prter2 39141 2llnmat 39784 2lnat 40044 cdlemefrs29bpre1 40657 elnn0rabdioph 43045 fiphp3d 43061 minregex 43775 |
| Copyright terms: Public domain | W3C validator |