![]() |
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 1863 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | df-rex 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 = 𝐴)) | |
3 | dfclel 2810 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 1, 2, 3 | 3bitr4ri 304 | 1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 𝑥 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ∃wrex 3069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-clel 2809 df-rex 3070 |
This theorem is referenced by: nelb 3230 nelbOLD 3231 ceqsralv 3513 clel5 3655 reueq 3733 reuind 3749 0el 4360 iunidOLD 5064 reusv3 5403 elidinxp 6043 sucel 6438 fvmptt 7018 releldm2 8033 qsid 8783 ttrcltr 9717 zorng 10505 rereccl 11939 nndiv 12265 incexc2 15791 ruclem12 16191 conjnmzb 19174 pgpfac1lem2 19993 pgpfac1lem4 19996 mat1dimelbas 22293 mat1dimbas 22294 chmaidscmat 22670 unisngl 23351 fmid 23784 dcubic 26692 addsrid 27794 addsprop 27806 negsprop 27860 mulsrid 27926 mulsprop 27943 fusgrn0degnn0 29189 chscllem2 31324 disjunsn 32258 grplsm0l 32953 ballotlemsima 33978 dfon2lem8 35232 brimg 35379 dfrecs2 35392 altopelaltxp 35418 prtlem9 38198 prter2 38215 2llnmat 38859 2lnat 39119 cdlemefrs29bpre1 39732 elnn0rabdioph 42004 fiphp3d 42020 minregex 42748 |
Copyright terms: Public domain | W3C validator |