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 5960

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 5957	. . . 4 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴))
3		df-br 5069	. . . 4 ⊢ (𝐵^◡𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ ^◡𝐴)
4	2, 3	syl6bbr 291	. . 3 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (^◡𝐴 “ {𝐵}) ↔ 𝐵^◡𝐴𝐶))
5		brcnvg 5752	. . 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 3496 {csn 4569 ⟨cop 4575 class class class wbr 5068 ^◡ccnv 5556 “ cima 5560

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 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332

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 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-br 5069 df-opab 5131 df-xp 5563 df-cnv 5565 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570

This theorem is referenced by: epini 5961 iniseg 5962 dfco2a 6101 elpred 6163 isomin 7092 isoini 7093 fnse 7829 infxpenlem 9441 fpwwe2lem8 10061 fpwwe2lem12 10065 fpwwe2lem13 10066 fpwwe2 10067 canth4 10071 canthwelem 10074 pwfseqlem4 10086 fz1isolem 13822 itg1addlem4 24302 elnlfn 29707 pw2f1ocnv 39641

W3C validator