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 5635

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 5632	. . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴))
3		df-br 4785	. . . 4 ⊢ (𝐵^◡𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴)
4	2, 3	syl6bbr 278	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐵^◡𝐴𝐶))
5		brcnvg 5441	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐵^◡𝐴𝐶 ↔ 𝐶𝐴𝐵))
6	4, 5	bitrd 268	. 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
7	1, 6	mpan2 663	1 ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∈ wcel 2144 Vcvv 3349 {csn 4314 ⟨cop 4320 class class class wbr 4784 ^◡ccnv 5248 “ cima 5252

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-sep 4912 ax-nul 4920 ax-pr 5034

This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3an 1072 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ral 3065 df-rex 3066 df-rab 3069 df-v 3351 df-sbc 3586 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-nul 4062 df-if 4224 df-sn 4315 df-pr 4317 df-op 4321 df-br 4785 df-opab 4845 df-xp 5255 df-cnv 5257 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262

This theorem is referenced by: epini 5636 iniseg 5637 dfco2a 5779 elpred 5836 isomin 6729 isoini 6730 fnse 7444 infxpenlem 9035 fpwwe2lem8 9660 fpwwe2lem12 9664 fpwwe2lem13 9665 fpwwe2 9666 canth4 9670 canthwelem 9673 pwfseqlem4 9685 fz1isolem 13446 itg1addlem4 23685 elnlfn 29121 pw2f1ocnv 38123

W3C validator