eliniseg - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > eliniseg		Structured version Visualization version GIF version

Theorem eliniseg 5482

Description: Membership in an initial segment. The idiom (^◡𝐴 “ {𝐵}), meaning {𝑥 ∣ 𝑥𝐴𝐵}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

**Hypothesis**
Ref	Expression
eliniseg.1	⊢ 𝐶 ∈ V

**Assertion**
Ref	Expression
eliniseg	⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))

**Proof of Theorem eliniseg**
Step	Hyp	Ref	Expression
1		eliniseg.1	. 2 ⊢ 𝐶 ∈ V
2		elimasng 5479	. . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴))
3		df-br 4645	. . . 4 ⊢ (𝐵^◡𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴)
4	2, 3	syl6bbr 278	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐵^◡𝐴𝐶))
5		brcnvg 5292	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐵^◡𝐴𝐶 ↔ 𝐶𝐴𝐵))
6	4, 5	bitrd 268	. 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
7	1, 6	mpan2 706	1 ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∈ wcel 1988 Vcvv 3195 {csn 4168 ⟨cop 4174 class class class wbr 4644 ^◡ccnv 5103 “ cima 5107

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1720 ax-4 1735 ax-5 1837 ax-6 1886 ax-7 1933 ax-9 1997 ax-10 2017 ax-11 2032 ax-12 2045 ax-13 2244 ax-ext 2600 ax-sep 4772 ax-nul 4780 ax-pr 4897

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1038 df-tru 1484 df-ex 1703 df-nf 1708 df-sb 1879 df-eu 2472 df-mo 2473 df-clab 2607 df-cleq 2613 df-clel 2616 df-nfc 2751 df-ral 2914 df-rex 2915 df-rab 2918 df-v 3197 df-sbc 3430 df-dif 3570 df-un 3572 df-in 3574 df-ss 3581 df-nul 3908 df-if 4078 df-sn 4169 df-pr 4171 df-op 4175 df-br 4645 df-opab 4704 df-xp 5110 df-cnv 5112 df-dm 5114 df-rn 5115 df-res 5116 df-ima 5117

This theorem is referenced by: epini 5483 iniseg 5484 dfco2a 5623 elpred 5681 isomin 6572 isoini 6573 fnse 7279 infxpenlem 8821 fpwwe2lem8 9444 fpwwe2lem12 9448 fpwwe2lem13 9449 fpwwe2 9450 canth4 9454 canthwelem 9457 pwfseqlem4 9469 fz1isolem 13228 itg1addlem4 23447 elnlfn 28757 pw2f1ocnv 37423

W3C validator