|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > riotaeqbidv | Structured version Visualization version GIF version | ||
| Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 15-Sep-2011.) | 
| Ref | Expression | 
|---|---|
| riotaeqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) | 
| riotaeqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | 
| Ref | Expression | 
|---|---|
| riotaeqbidv | ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | riotaeqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | riotabidv 7391 | . 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) | 
| 3 | riotaeqbidv.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 3 | riotaeqdv 7390 | . 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥 ∈ 𝐵 𝜒)) | 
| 5 | 2, 4 | eqtrd 2776 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 ℩crio 7388 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-ss 3967 df-uni 4907 df-iota 6513 df-riota 7389 | 
| This theorem is referenced by: dfoi 9552 oieq1 9553 oieq2 9554 ordtypecbv 9558 ordtypelem3 9561 zorn2lem1 10537 zorn2g 10544 cidfval 17720 cidval 17721 cidpropd 17754 lubfval 18396 glbfval 18409 grpinvfval 18997 grpinvfvalALT 18998 pj1fval 19713 mpfrcl 22110 evlsval 22111 q1pval 26195 ig1pval 26216 scutval 27846 mirval 28664 midf 28785 ismidb 28787 lmif 28794 islmib 28796 gidval 30532 grpoinvfval 30542 pjhfval 31416 cvmliftlem5 35295 cvmliftlem15 35304 weiunlem2 36465 trlfset 40163 dicffval 41177 dicfval 41178 dihffval 41233 dihfval 41234 hvmapffval 41761 hvmapfval 41762 hdmap1fval 41799 hdmapffval 41829 hdmapfval 41830 hgmapfval 41889 wessf1ornlem 45195 | 
| Copyright terms: Public domain | W3C validator |