![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > riotabidv | Structured version Visualization version GIF version |
Description: Formula-building deduction for restricted iota. (Contributed by NM, 15-Sep-2011.) |
Ref | Expression |
---|---|
riotabidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
riotabidv | ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | riotabidv.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | anbi2d 619 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | iotabidv 6170 | . 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-riota 6935 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-riota 6935 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3eqtr4g 2833 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ℩cio 6147 ℩crio 6934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-rex 3088 df-uni 4709 df-iota 6149 df-riota 6935 |
This theorem is referenced by: riotaeqbidv 6938 csbriota 6947 sup0riota 8722 infval 8743 fin23lem27 9546 subval 10675 divval 11099 flval 12977 ceilval2 13023 cjval 14320 sqrtval 14455 qnumval 15931 qdenval 15932 lubval 17464 glbval 17477 joinval2 17489 meetval2 17503 grpinvval 17943 pj1fval 18590 pj1val 18591 q1pval 24462 coeval 24528 quotval 24596 ismidb 26278 lmif 26285 islmib 26287 uspgredg2v 26721 usgredg2v 26724 frgrncvvdeqlem8 27852 frgrncvvdeqlem9 27853 grpoinvval 28089 pjhval 28967 nmopadjlei 29658 cdj3lem2 30005 cvmliftlem15 32159 cvmlift2lem4 32167 cvmlift2 32177 cvmlift3lem2 32181 cvmlift3lem4 32183 cvmlift3lem6 32185 cvmlift3lem7 32186 cvmlift3lem9 32188 cvmlift3 32189 fvtransport 33043 lshpkrlem1 35720 lshpkrlem2 35721 lshpkrlem3 35722 lshpkrcl 35726 trlset 36771 trlval 36772 cdleme27b 36978 cdleme29b 36985 cdleme31so 36989 cdleme31sn1 36991 cdleme31sn1c 36998 cdleme31fv 37000 cdlemefrs29clN 37009 cdleme40v 37079 cdlemg1cN 37197 cdlemg1cex 37198 cdlemksv 37454 cdlemkuu 37505 cdlemkid3N 37543 cdlemkid4 37544 cdlemm10N 37728 dicval 37786 dihval 37842 dochfl1 38086 lcfl7N 38111 lcfrlem8 38159 lcfrlem9 38160 lcf1o 38161 mapdhval 38334 hvmapval 38370 hvmapvalvalN 38371 hdmap1fval 38406 hdmap1vallem 38407 hdmap1val 38408 hdmap1cbv 38412 hdmapfval 38437 hdmapval 38438 hgmapffval 38495 hgmapfval 38496 hgmapval 38497 resubval 38658 unxpwdom3 39120 mpaaval 39176 |
Copyright terms: Public domain | W3C validator |