| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > riota2 | Structured version Visualization version GIF version | ||
| Description: This theorem shows a condition that allows to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.) |
| Ref | Expression |
|---|---|
| riota2.1 | ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| riota2 | ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv 2905 | . 2 ⊢ Ⅎ𝑥𝐵 | |
| 2 | nfv 1914 | . 2 ⊢ Ⅎ𝑥𝜓 | |
| 3 | riota2.1 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | |
| 4 | 1, 2, 3 | riota2f 7412 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∃!wreu 3378 ℩crio 7387 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-reu 3381 df-v 3482 df-un 3956 df-ss 3968 df-sn 4627 df-pr 4629 df-uni 4908 df-iota 6514 df-riota 7388 |
| This theorem is referenced by: eqsup 9496 sup0 9506 ttrcltr 9756 fin23lem22 10367 subadd 11511 divmul 11925 fllelt 13837 flflp1 13847 flval2 13854 flbi 13856 remim 15156 resqrtcl 15292 resqrtthlem 15293 sqrtneg 15306 sqrtthlem 15401 divalgmod 16443 qnumdenbi 16781 catidd 17723 lubprop 18403 glbprop 18416 poslubd 18458 isglbd 18554 ismgmid 18678 isgrpinv 19011 pj1id 19717 coeeq 26266 scutbday 27849 eqscut 27850 scutun12 27855 scutbdaylt 27863 divsmulw 28218 ismir 28667 mireq 28673 ismidb 28786 islmib 28795 usgredg2vlem2 29243 frgrncvvdeqlem3 30320 frgr2wwlkeqm 30350 cnidOLD 30601 hilid 31180 pjpreeq 31417 cnvbraval 32129 cdj3lem2 32454 xdivmul 32907 cvmliftphtlem 35322 cvmlift3lem4 35327 cvmlift3lem6 35329 cvmlift3lem9 35332 transportprops 36035 ltflcei 37615 cmpidelt 37866 exidresid 37886 lshpkrlem1 39111 cdlemeiota 40587 dochfl1 41478 hgmapvs 41893 renegadd 42402 resubadd 42409 addinvcom 42461 evlsval3 42569 fsuppind 42600 wessf1ornlem 45190 fourierdlem50 46171 |
| Copyright terms: Public domain | W3C validator |