| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ecelqsi | Structured version Visualization version GIF version | ||
| Description: Membership of an equivalence class in a quotient set. (Contributed by NM, 25-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| Ref | Expression |
|---|---|
| ecelqsi.1 | ⊢ 𝑅 ∈ V |
| Ref | Expression |
|---|---|
| ecelqsi | ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ecelqsi.1 | . 2 ⊢ 𝑅 ∈ V | |
| 2 | ecelqsw 8754 | . 2 ⊢ ((𝑅 ∈ V ∧ 𝐵 ∈ 𝐴) → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) | |
| 3 | 1, 2 | mpan 702 | 1 ⊢ (𝐵 ∈ 𝐴 → [𝐵]𝑅 ∈ (𝐴 / 𝑅)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2145 Vcvv 3457 [cec 8680 / cqs 8681 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-ext 2737 ax-sep 5250 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-sb 2094 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-xp 5657 df-rel 5658 df-cnv 5659 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-ec 8684 df-qs 8688 |
| This theorem is referenced by: ecopqsi 8756 addsrpr 11048 mulsrpr 11049 0r 11053 1sr 11054 m1r 11055 addclsr 11056 mulclsr 11057 quseccl0 19244 ghmqusnsglem1 19338 ghmquskerlem1 19341 ghmquskerco 19342 ghmqusker 19345 orbsta 19371 frgpeccl 19819 rngqiprngimf 21396 qsidomlem1 21437 qustgphaus 24237 vitalilem2 25725 vitalilem3 25726 rloccring 33499 rloc0g 33500 rloc1r 33501 rlocf1 33502 rlocinvunit 33503 rlocisunit 33504 fracfld 33539 nsgqusf1olem1 33633 qsdrngilem 33688 qsdrngi 33689 qsdrnglem2 33690 zringfrac 33756 pstmfval 34198 |
| Copyright terms: Public domain | W3C validator |