![]() |
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 1905 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | df-rex 3096 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
3 | df-clel 2774 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 1, 2, 3 | 3bitr4ri 296 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 = wceq 1601 ∃wex 1823 ∈ wcel 2107 ∃wrex 3091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-clel 2774 df-rex 3096 |
This theorem is referenced by: clel5 3547 reueq 3618 reuind 3628 0el 4169 iunid 4810 reusv3 5119 elidinxp 5707 sucel 6051 fvmptt 6563 releldm2 7499 qsid 8098 zorng 9663 rereccl 11096 nndiv 11426 zqOLD 12107 incexc2 14983 ruclem12 15383 conjnmzb 18090 pgpfac1lem2 18872 pgpfac1lem4 18875 mat1dimelbas 20693 mat1dimbas 20694 chmaidscmat 21071 unisngl 21750 fmid 22183 dcubic 25035 fusgrn0degnn0 26864 chscllem2 29086 disjunsn 29987 ballotlemsima 31184 dfon2lem8 32291 brimg 32641 dfrecs2 32654 altopelaltxp 32680 prtlem9 35027 prtlem11 35029 prter2 35044 2llnmat 35687 2lnat 35947 cdlemefrs29bpre1 36560 elnn0rabdioph 38341 fiphp3d 38357 |
Copyright terms: Public domain | W3C validator |