![]() |
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 2908 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | nfv 1918 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | riota2.1 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | riota2f 7339 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃!wreu 3352 ℩crio 7313 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ral 3066 df-rex 3075 df-reu 3355 df-v 3448 df-un 3916 df-in 3918 df-ss 3928 df-sn 4588 df-pr 4590 df-uni 4867 df-iota 6449 df-riota 7314 |
This theorem is referenced by: eqsup 9393 sup0 9403 ttrcltr 9653 fin23lem22 10264 subadd 11405 divmul 11817 fllelt 13703 flflp1 13713 flval2 13720 flbi 13722 remim 15003 resqrtcl 15139 resqrtthlem 15140 sqrtneg 15153 sqrtthlem 15248 divalgmod 16289 qnumdenbi 16620 catidd 17561 lubprop 18248 glbprop 18261 poslubd 18303 isglbd 18399 ismgmid 18521 isgrpinv 18805 pj1id 19482 coeeq 25591 scutbday 27146 eqscut 27147 scutun12 27152 scutbdaylt 27160 ismir 27604 mireq 27610 ismidb 27723 islmib 27732 usgredg2vlem2 28177 frgrncvvdeqlem3 29248 frgr2wwlkeqm 29278 cnidOLD 29527 hilid 30106 pjpreeq 30343 cnvbraval 31055 cdj3lem2 31380 xdivmul 31784 cvmliftphtlem 33914 cvmlift3lem4 33919 cvmlift3lem6 33921 cvmlift3lem9 33924 transportprops 34622 ltflcei 36069 cmpidelt 36321 exidresid 36341 lshpkrlem1 37575 cdlemeiota 39051 dochfl1 39942 hgmapvs 40357 evlsval3 40747 fsuppind 40768 renegadd 40844 resubadd 40851 addinvcom 40903 wessf1ornlem 43410 fourierdlem50 44404 |
Copyright terms: Public domain | W3C validator |