Theorem eliniseg 6104

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.)

Hypothesis

Ref	Expression
eliniseg.1	⊢ 𝐶 ∈ V

Assertion

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

Proof of Theorem eliniseg

Step	Hyp	Ref	Expression
1		eliniseg.1	. 2 ⊢ 𝐶 ∈ V
2		elinisegg 6103	. 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ V) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))
3	1, 2	mpan2 704	1 ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147  Vcvv 3454  {csn 4588   class class class wbr 5106  ^◡ccnv 5654   “ cima 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  epin  6105  iniseg  6107  dfco2a  6260  isomin  7368  isoini  7369  fnse  8177  infxpenlem  10119  fpwwe2lem7  10749  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  canth4  10759  canthwelem  10762  pwfseqlem4  10774  fz1isolem  14633  itg1addlem4  26050  elnlfn  32560  j0ltalephlem  36007  pw2f1ocnv  44237  relpmin  46137  inisegn0a  50152