![]() |
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 628 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | iotabidv 6538 | . 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-riota 7380 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-riota 7380 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3eqtr4g 2791 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ℩cio 6504 ℩crio 7379 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-ss 3964 df-uni 4914 df-iota 6506 df-riota 7380 |
This theorem is referenced by: riotaeqbidv 7383 csbriota 7396 sup0riota 9508 infval 9529 ttrcltr 9759 fin23lem27 10371 subval 11501 divval 11925 flval 13814 ceilval2 13860 cjval 15107 sqrtval 15242 qnumval 16739 qdenval 16740 lubval 18381 glbval 18394 joinval2 18406 meetval2 18420 grpinvval 18975 pj1fval 19692 pj1val 19693 q1pval 26182 coeval 26250 quotval 26320 divsval 28190 ismidb 28705 lmif 28712 islmib 28714 uspgredg2v 29160 usgredg2v 29163 frgrncvvdeqlem8 30239 frgrncvvdeqlem9 30240 grpoinvval 30456 pjhval 31330 nmopadjlei 32021 cdj3lem2 32368 cvmliftlem15 35126 cvmlift2lem4 35134 cvmlift2 35144 cvmlift3lem2 35148 cvmlift3lem4 35150 cvmlift3lem6 35152 cvmlift3lem7 35153 cvmlift3lem9 35155 cvmlift3 35156 fvtransport 35856 lshpkrlem1 38808 lshpkrlem2 38809 lshpkrlem3 38810 lshpkrcl 38814 trlset 39860 trlval 39861 cdleme27b 40067 cdleme29b 40074 cdleme31so 40078 cdleme31sn1 40080 cdleme31sn1c 40087 cdleme31fv 40089 cdlemefrs29clN 40098 cdleme40v 40168 cdlemg1cN 40286 cdlemg1cex 40287 cdlemksv 40543 cdlemkuu 40594 cdlemkid3N 40632 cdlemkid4 40633 cdlemm10N 40817 dicval 40875 dihval 40931 dochfl1 41175 lcfl7N 41200 lcfrlem8 41248 lcfrlem9 41249 lcf1o 41250 mapdhval 41423 hvmapval 41459 hvmapvalvalN 41460 hdmap1fval 41495 hdmap1vallem 41496 hdmap1val 41497 hdmap1cbv 41501 hdmapfval 41526 hdmapval 41527 hgmapffval 41584 hgmapfval 41585 hgmapval 41586 resubval 42147 unxpwdom3 42756 mpaaval 42812 |
Copyright terms: Public domain | W3C validator |