![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > riotabidva | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (rabbidva 3438 analog.) (Contributed by NM, 17-Jan-2012.) |
Ref | Expression |
---|---|
riotabidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
riotabidva | ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | riotabidva.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
2 | 1 | pm5.32da 578 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒))) |
3 | 2 | iotabidv 6528 | . 2 ⊢ (𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒))) |
4 | df-riota 7368 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
5 | df-riota 7368 | . 2 ⊢ (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜒)) | |
6 | 3, 4, 5 | 3eqtr4g 2796 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1540 ∈ wcel 2105 ℩cio 6494 ℩crio 7367 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3956 df-ss 3966 df-uni 4910 df-iota 6496 df-riota 7368 |
This theorem is referenced by: riotabiia 7389 dfceil2 13809 cidpropd 17659 grpinvpropd 18935 mirval 28170 mirfv 28171 grpoidval 30030 adjval2 31408 riotaeqbidva 32000 xdivval 32349 toslub 32407 tosglb 32409 ringinvval 32651 glbconN 38551 glbconNOLD 38552 cdlemk33N 40084 cdlemk34 40085 cdlemkid4 40109 |
Copyright terms: Public domain | W3C validator |