![]() |
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 1859 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
3 | dfclel 2815 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 1, 2, 3 | 3bitr4ri 304 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1537 ∃wex 1776 ∈ wcel 2106 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-clel 2814 df-rex 3069 |
This theorem is referenced by: nelb 3232 nelbOLD 3233 ceqsralv 3520 clel5 3665 reueq 3746 reuind 3762 0el 4369 iunidOLD 5066 reusv3 5411 elidinxp 6064 sucel 6460 fvmptt 7036 releldm2 8067 qsid 8822 ttrcltr 9754 zorng 10542 rereccl 11983 nndiv 12310 incexc2 15871 ruclem12 16274 conjnmzb 19284 pgpfac1lem2 20110 pgpfac1lem4 20113 mat1dimelbas 22493 mat1dimbas 22494 chmaidscmat 22870 unisngl 23551 fmid 23984 dcubic 26904 addsrid 28012 addsprop 28024 negsprop 28082 mulsrid 28154 mulsprop 28171 fusgrn0degnn0 29532 chscllem2 31667 disjunsn 32614 grplsm0l 33411 ballotlemsima 34497 dfon2lem8 35772 brimg 35919 dfrecs2 35932 altopelaltxp 35958 prtlem9 38846 prter2 38863 2llnmat 39507 2lnat 39767 cdlemefrs29bpre1 40380 elnn0rabdioph 42791 fiphp3d 42807 minregex 43524 |
Copyright terms: Public domain | W3C validator |