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 1774 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | df-rex 2902 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
3 | df-clel 2606 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 1, 2, 3 | 3bitr4ri 292 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-clel 2606 df-rex 2902 |
This theorem is referenced by: reueq 3371 reuind 3378 0el 3895 iunid 4511 reusv3 4802 sucel 5715 fvmptt 6208 releldm2 7109 qsid 7700 zorng 9209 rereccl 10622 nndiv 10938 zq 11670 4fvwrd4 12328 wrdlen1 13198 incexc2 14409 ruclem12 14809 phisum 15333 conjnmzb 17518 symgmov1 17635 pgpfac1lem2 18297 pgpfac1lem4 18300 mat1dimelbas 20096 mat1dimbas 20097 chmaidscmat 20472 unisngl 21140 fmid 21574 dcubic 24373 usgn0fidegnn0 26556 chscllem2 27881 disjunsn 28789 ballotlemsima 29904 dfon2lem8 30939 brimg 31214 dfrecs2 31227 altopelaltxp 31253 prtlem9 33167 prtlem11 33169 prter2 33184 2llnmat 33828 2lnat 34088 cdlemefrs29bpre1 34703 elnn0rabdioph 36385 fiphp3d 36401 fusgrn0degnn0 40714 |
Copyright terms: Public domain | W3C validator |