![]() |
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 us 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 2947 | . 2 ⊢ Ⅎ𝑥𝐵 | |
2 | nfv 1890 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | riota2.1 | . 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | riota2f 6989 | 1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1520 ∈ wcel 2079 ∃!wreu 3105 ℩crio 6967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-10 2110 ax-11 2124 ax-12 2139 ax-13 2342 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1080 df-tru 1523 df-ex 1760 df-nf 1764 df-sb 2041 df-mo 2574 df-eu 2610 df-clab 2774 df-cleq 2786 df-clel 2861 df-nfc 2933 df-ral 3108 df-rex 3109 df-reu 3110 df-v 3434 df-sbc 3702 df-un 3859 df-sn 4467 df-pr 4469 df-uni 4740 df-iota 6181 df-riota 6968 |
This theorem is referenced by: eqsup 8756 sup0 8766 fin23lem22 9584 subadd 10725 divmul 11138 fllelt 13005 flflp1 13015 flval2 13022 flbi 13024 remim 14298 resqrtcl 14435 resqrtthlem 14436 sqrtneg 14449 sqrtthlem 14544 divalgmod 15578 qnumdenbi 15901 catidd 16768 lubprop 17413 glbprop 17426 isglbd 17544 poslubd 17575 ismgmid 17691 isgrpinv 17901 pj1id 18540 coeeq 24488 ismir 26115 mireq 26121 ismidb 26234 islmib 26243 usgredg2vlem2 26679 frgrncvvdeqlem3 27760 frgr2wwlkeqm 27790 cnidOLD 28038 hilid 28617 pjpreeq 28854 cnvbraval 29566 cdj3lem2 29891 xdivmul 30256 cvmliftphtlem 32128 cvmlift3lem4 32133 cvmlift3lem6 32135 cvmlift3lem9 32138 scutbday 32821 scutun12 32825 scutbdaylt 32830 transportprops 33049 ltflcei 34357 cmpidelt 34615 exidresid 34635 lshpkrlem1 35727 cdlemeiota 37202 dochfl1 38093 hgmapvs 38508 renegadd 38674 resubadd 38682 wessf1ornlem 40938 fourierdlem50 41937 |
Copyright terms: Public domain | W3C validator |