![]() |
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 6867 | . 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
3 | riotaeqbidv.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | riotaeqdv 6866 | . 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥 ∈ 𝐵 𝜒)) |
5 | 2, 4 | eqtrd 2860 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1658 ℩crio 6864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-rex 3122 df-uni 4658 df-iota 6085 df-riota 6865 |
This theorem is referenced by: dfoi 8684 oieq1 8685 oieq2 8686 ordtypecbv 8690 ordtypelem3 8693 zorn2lem1 9632 zorn2g 9639 cidfval 16688 cidval 16689 cidpropd 16721 lubfval 17330 glbfval 17343 grpinvfval 17813 pj1fval 18457 mpfrcl 19877 evlsval 19878 q1pval 24311 ig1pval 24330 mirval 25966 midf 26084 ismidb 26086 lmif 26093 islmib 26095 gidval 27921 grpoinvfval 27931 pjhfval 28809 cvmliftlem5 31816 cvmliftlem15 31825 scutval 32449 trlfset 36234 dicffval 37248 dicfval 37249 dihffval 37304 dihfval 37305 hvmapffval 37832 hvmapfval 37833 hdmap1fval 37870 hdmapffval 37900 hdmapfval 37901 hgmapfval 37960 wessf1ornlem 40178 |
Copyright terms: Public domain | W3C validator |