Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > riotabidv | Structured version Visualization version GIF version |
Description: Formula-building deduction rule 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 736 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | iotabidv 5789 | . 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-riota 6511 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-riota 6511 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3eqtr4g 2669 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ℩cio 5766 ℩crio 6510 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-uni 4373 df-iota 5768 df-riota 6511 |
This theorem is referenced by: riotaeqbidv 6514 csbriota 6523 sup0riota 8254 infval 8275 fin23lem27 9033 subval 10151 divval 10566 flval 12457 ceilval2 12503 cjval 13690 sqrtval 13825 qnumval 15283 qdenval 15284 lubval 16807 glbval 16820 joinval2 16832 meetval2 16846 grpinvval 17284 pj1fval 17930 pj1val 17931 q1pval 23717 coeval 23783 quotval 23851 ismidb 25470 lmif 25477 islmib 25479 usgraidx2v 25922 nbgraf1olem4 25973 frgrancvvdeqlemB 26565 frgrancvvdeqlemC 26566 grpoinvval 26761 pjhval 27640 nmopadjlei 28331 cdj3lem2 28678 cvmliftlem15 30534 cvmlift2lem4 30542 cvmlift2 30552 cvmlift3lem2 30556 cvmlift3lem4 30558 cvmlift3lem6 30560 cvmlift3lem7 30561 cvmlift3lem9 30563 cvmlift3 30564 fvtransport 31309 lshpkrlem1 33415 lshpkrlem2 33416 lshpkrlem3 33417 lshpkrcl 33421 trlset 34466 trlval 34467 cdleme27b 34674 cdleme29b 34681 cdleme31so 34685 cdleme31sn1 34687 cdleme31sn1c 34694 cdleme31fv 34696 cdlemefrs29clN 34705 cdleme40v 34775 cdlemg1cN 34893 cdlemg1cex 34894 cdlemksv 35150 cdlemkuu 35201 cdlemkid3N 35239 cdlemkid4 35240 cdlemm10N 35425 dicval 35483 dihval 35539 dochfl1 35783 lcfl7N 35808 lcfrlem8 35856 lcfrlem9 35857 lcf1o 35858 mapdhval 36031 hvmapval 36067 hvmapvalvalN 36068 hdmap1fval 36104 hdmap1vallem 36105 hdmap1val 36106 hdmap1cbv 36110 hdmapfval 36137 hdmapval 36138 hgmapffval 36195 hgmapfval 36196 hgmapval 36197 unxpwdom3 36683 mpaaval 36740 uspgredg2v 40451 usgredg2v 40454 frgrncvvdeqlemB 41477 frgrncvvdeqlemC 41478 |
Copyright terms: Public domain | W3C validator |