![]() |
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 2904 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | nfv 1918 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | riota2.1 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | riota2f 7384 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃!wreu 3375 ℩crio 7358 |
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 2704 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-reu 3378 df-v 3477 df-un 3951 df-in 3953 df-ss 3963 df-sn 4627 df-pr 4629 df-uni 4907 df-iota 6491 df-riota 7359 |
This theorem is referenced by: eqsup 9446 sup0 9456 ttrcltr 9706 fin23lem22 10317 subadd 11458 divmul 11870 fllelt 13757 flflp1 13767 flval2 13774 flbi 13776 remim 15059 resqrtcl 15195 resqrtthlem 15196 sqrtneg 15209 sqrtthlem 15304 divalgmod 16344 qnumdenbi 16675 catidd 17619 lubprop 18306 glbprop 18319 poslubd 18361 isglbd 18457 ismgmid 18579 isgrpinv 18873 pj1id 19559 coeeq 25722 scutbday 27284 eqscut 27285 scutun12 27290 scutbdaylt 27298 divsmulw 27619 ismir 27889 mireq 27895 ismidb 28008 islmib 28017 usgredg2vlem2 28462 frgrncvvdeqlem3 29533 frgr2wwlkeqm 29563 cnidOLD 29812 hilid 30391 pjpreeq 30628 cnvbraval 31340 cdj3lem2 31665 xdivmul 32068 cvmliftphtlem 34245 cvmlift3lem4 34250 cvmlift3lem6 34252 cvmlift3lem9 34255 transportprops 34943 ltflcei 36413 cmpidelt 36664 exidresid 36684 lshpkrlem1 37917 cdlemeiota 39393 dochfl1 40284 hgmapvs 40699 evlsval3 41080 fsuppind 41111 renegadd 41188 resubadd 41195 addinvcom 41247 wessf1ornlem 43814 fourierdlem50 44806 |
Copyright terms: Public domain | W3C validator |