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 5944

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 5941	. . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴))
3		df-br 5053	. . . 4 ⊢ (𝐵^◡𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴)
4	2, 3	syl6bbr 291	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐵^◡𝐴𝐶))
5		brcnvg 5736	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐵^◡𝐴𝐶 ↔ 𝐶𝐴𝐵))
6	4, 5	bitrd 281	. 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
7	1, 6	mpan2 689	1 ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∈ wcel 2114 Vcvv 3486 {csn 4553 ⟨cop 4559 class class class wbr 5052 ^◡ccnv 5540 “ cima 5544

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pr 5316

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3488 df-sbc 3764 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-sn 4554 df-pr 4556 df-op 4560 df-br 5053 df-opab 5115 df-xp 5547 df-cnv 5549 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554

This theorem is referenced by: epini 5945 iniseg 5946 dfco2a 6085 elpred 6147 isomin 7076 isoini 7077 fnse 7813 infxpenlem 9425 fpwwe2lem8 10045 fpwwe2lem12 10049 fpwwe2lem13 10050 fpwwe2 10051 canth4 10055 canthwelem 10058 pwfseqlem4 10070 fz1isolem 13809 itg1addlem4 24283 elnlfn 29689 pw2f1ocnv 39726

W3C validator