![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eliniseg | Structured version Visualization version GIF version |
Description: Membership in the inverse image of a singleton. An application is to express initial segments for an order relation. See for example Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
eliniseg.1 | ⊢ 𝐶 ∈ V |
Ref | Expression |
---|---|
eliniseg | ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliniseg.1 | . 2 ⊢ 𝐶 ∈ V | |
2 | elinisegg 6081 | . 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | |
3 | 1, 2 | mpan2 689 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2106 Vcvv 3473 {csn 4622 class class class wbr 5141 ◡ccnv 5668 “ cima 5672 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-br 5142 df-opab 5204 df-xp 5675 df-cnv 5677 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 |
This theorem is referenced by: epin 6083 iniseg 6085 dfco2a 6234 isomin 7318 isoini 7319 fnse 8101 infxpenlem 9990 fpwwe2lem7 10614 fpwwe2lem11 10618 fpwwe2lem12 10619 fpwwe2 10620 canth4 10624 canthwelem 10627 pwfseqlem4 10639 fz1isolem 14404 itg1addlem4 25145 itg1addlem4OLD 25146 elnlfn 31044 pw2f1ocnv 41547 |
Copyright terms: Public domain | W3C validator |