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 7105 | . 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐴 𝜒)) |
3 | riotaeqbidv.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | riotaeqdv 7104 | . 2 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜒) = (℩𝑥 ∈ 𝐵 𝜒)) |
5 | 2, 4 | eqtrd 2853 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = (℩𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ℩crio 7102 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rex 3141 df-uni 4831 df-iota 6307 df-riota 7103 |
This theorem is referenced by: dfoi 8963 oieq1 8964 oieq2 8965 ordtypecbv 8969 ordtypelem3 8972 zorn2lem1 9906 zorn2g 9913 cidfval 16935 cidval 16936 cidpropd 16968 lubfval 17576 glbfval 17589 grpinvfval 18080 grpinvfvalALT 18081 pj1fval 18749 mpfrcl 20226 evlsval 20227 q1pval 24674 ig1pval 24693 mirval 26368 midf 26489 ismidb 26491 lmif 26498 islmib 26500 gidval 28216 grpoinvfval 28226 pjhfval 29100 cvmliftlem5 32433 cvmliftlem15 32442 scutval 33162 trlfset 37176 dicffval 38190 dicfval 38191 dihffval 38246 dihfval 38247 hvmapffval 38774 hvmapfval 38775 hdmap1fval 38812 hdmapffval 38842 hdmapfval 38843 hgmapfval 38902 wessf1ornlem 41321 |
Copyright terms: Public domain | W3C validator |