![]() |
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 2903 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | nfv 1917 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | riota2.1 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | riota2f 7392 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃!wreu 3374 ℩crio 7366 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 df-reu 3377 df-v 3476 df-un 3953 df-in 3955 df-ss 3965 df-sn 4629 df-pr 4631 df-uni 4909 df-iota 6495 df-riota 7367 |
This theorem is referenced by: eqsup 9453 sup0 9463 ttrcltr 9713 fin23lem22 10324 subadd 11467 divmul 11879 fllelt 13766 flflp1 13776 flval2 13783 flbi 13785 remim 15068 resqrtcl 15204 resqrtthlem 15205 sqrtneg 15218 sqrtthlem 15313 divalgmod 16353 qnumdenbi 16684 catidd 17628 lubprop 18315 glbprop 18328 poslubd 18370 isglbd 18466 ismgmid 18590 isgrpinv 18914 pj1id 19608 coeeq 25965 scutbday 27530 eqscut 27531 scutun12 27536 scutbdaylt 27544 divsmulw 27867 ismir 28165 mireq 28171 ismidb 28284 islmib 28293 usgredg2vlem2 28738 frgrncvvdeqlem3 29809 frgr2wwlkeqm 29839 cnidOLD 30090 hilid 30669 pjpreeq 30906 cnvbraval 31618 cdj3lem2 31943 xdivmul 32346 cvmliftphtlem 34594 cvmlift3lem4 34599 cvmlift3lem6 34601 cvmlift3lem9 34604 transportprops 35298 ltflcei 36779 cmpidelt 37030 exidresid 37050 lshpkrlem1 38283 cdlemeiota 39759 dochfl1 40650 hgmapvs 41065 evlsval3 41433 fsuppind 41464 renegadd 41547 resubadd 41554 addinvcom 41606 wessf1ornlem 44183 fourierdlem50 45171 |
Copyright terms: Public domain | W3C validator |