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 1852 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | df-rex 3144 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
3 | dfclel 2894 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 1, 2, 3 | 3bitr4ri 305 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1528 ∃wex 1771 ∈ wcel 2105 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-clel 2893 df-rex 3144 |
This theorem is referenced by: nelb 3268 clel5 3656 reueq 3727 reuind 3743 0el 4319 iunid 4976 reusv3 5297 elidinxp 5905 sucel 6258 fvmptt 6781 releldm2 7733 qsid 8353 zorng 9915 rereccl 11347 nndiv 11672 zqOLD 12344 incexc2 15183 ruclem12 15584 conjnmzb 18333 pgpfac1lem2 19128 pgpfac1lem4 19131 mat1dimelbas 21010 mat1dimbas 21011 chmaidscmat 21386 unisngl 22065 fmid 22498 dcubic 25351 fusgrn0degnn0 27209 chscllem2 29343 disjunsn 30273 ballotlemsima 31673 dfon2lem8 32933 brimg 33296 dfrecs2 33309 altopelaltxp 33335 prtlem9 35882 prter2 35899 2llnmat 36542 2lnat 36802 cdlemefrs29bpre1 37415 elnn0rabdioph 39280 fiphp3d 39296 |
Copyright terms: Public domain | W3C validator |