|   | 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 1860 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 2 | df-rex 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
| 3 | dfclel 2816 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 4 | 1, 2, 3 | 3bitr4ri 304 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1539 ∃wex 1778 ∈ wcel 2107 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-clel 2815 df-rex 3070 | 
| This theorem is referenced by: nelb 3233 nelbOLD 3234 ceqsralv 3521 clel5 3664 reueq 3742 reuind 3758 0el 4362 iunidOLD 5060 reusv3 5404 elidinxp 6061 sucel 6457 fvmptt 7035 releldm2 8069 qsid 8824 ttrcltr 9757 zorng 10545 rereccl 11986 nndiv 12313 incexc2 15875 ruclem12 16278 conjnmzb 19272 pgpfac1lem2 20096 pgpfac1lem4 20099 mat1dimelbas 22478 mat1dimbas 22479 chmaidscmat 22855 unisngl 23536 fmid 23969 dcubic 26890 addsrid 27998 addsprop 28010 negsprop 28068 mulsrid 28140 mulsprop 28157 fusgrn0degnn0 29518 chscllem2 31658 disjunsn 32608 grplsm0l 33432 ballotlemsima 34519 dfon2lem8 35792 brimg 35939 dfrecs2 35952 altopelaltxp 35978 prtlem9 38866 prter2 38883 2llnmat 39527 2lnat 39787 cdlemefrs29bpre1 40400 elnn0rabdioph 42819 fiphp3d 42835 minregex 43552 | 
| Copyright terms: Public domain | W3C validator |