Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ecexg | Structured version Visualization version GIF version |
Description: An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.) |
Ref | Expression |
---|---|
ecexg | ⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ec 8398 | . 2 ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) | |
2 | imaexg 7698 | . 2 ⊢ (𝑅 ∈ 𝐵 → (𝑅 “ {𝐴}) ∈ V) | |
3 | 1, 2 | eqeltrid 2842 | 1 ⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 Vcvv 3413 {csn 4546 “ cima 5559 [cec 8394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5197 ax-nul 5204 ax-pr 5327 ax-un 7528 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3415 df-dif 3874 df-un 3876 df-in 3878 df-ss 3888 df-nul 4243 df-if 4445 df-sn 4547 df-pr 4549 df-op 4553 df-uni 4825 df-br 5059 df-opab 5121 df-xp 5562 df-cnv 5564 df-dm 5566 df-rn 5567 df-res 5568 df-ima 5569 df-ec 8398 |
This theorem is referenced by: ecelqsg 8459 uniqs 8464 eroveu 8499 erov 8501 addsrpr 10694 mulsrpr 10695 quslem 17053 eqgen 18602 qusghm 18664 sylow2blem1 19014 vrgpval 19162 znzrhval 20516 qustgpopn 23022 qustgplem 23023 elpi1 23947 pi1xfrval 23956 pi1xfrcnvlem 23958 pi1xfrcnv 23959 pi1cof 23961 pi1coval 23962 tgjustr 26570 qusker 31268 qusvscpbl 31270 qusscaval 31271 pstmfval 31565 fvline 34188 ecex2 36205 |
Copyright terms: Public domain | W3C validator |