Theorem fniniseg 7059

Description: Membership in the preimage of a singleton, under a function. (Contributed by Mario Carneiro, 12-May-2014.) (Proof shortened by Mario Carneiro , 28-Apr-2015.)

Assertion

Ref	Expression
fniniseg	⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Proof of Theorem fniniseg

Step	Hyp	Ref	Expression
1		elpreima 7057	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6898	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4598	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 635	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {csn 4583  ^◡ccnv 5649   “ cima 5653   Fn wfn 6533  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3899  df-un 3901  df-in 3903  df-ss 3914  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  fparlem1  8123  fparlem2  8124  pw2f1olem  9100  recmulnq  11049  dmrecnq  11053  indpi1  12334  vdwlem1  17159  vdwlem2  17160  vdwlem6  17164  vdwlem8  17166  vdwlem9  17167  vdwlem12  17170  vdwlem13  17171  ramval  17186  ramub1lem1  17204  ghmeqker  19457  ghmqusnsglem1  19494  ghmquskerlem1  19497  ghmqusker  19501  efgrelexlemb  19964  efgredeu  19966  psgnevpmb  21893  qtopeu  24035  itg1addlem1  26013  i1faddlem  26014  i1fmullem  26015  i1fmulclem  26023  i1fres  26026  itg10a  26031  itg1ge0a  26032  itg1climres  26035  mbfi1fseqlem4  26039  ply1remlem  26483  ply1rem  26484  fta1glem1  26486  fta1glem2  26487  fta1g  26488  fta1blem  26489  plyco0  26510  ofmulrt  26600  plyremlem  26625  plyrem  26626  fta1lem  26628  fta1  26629  rnplynfin  26630  plyconz  26631  vieta1lem1  26633  vieta1lem2  26634  vieta1  26635  plyexmo  26636  elaa  26639  aannenlem1  26655  aalioulem2  26660  pilem1  26778  efif1olem3  26872  efif1olem4  26873  efifo  26875  eff1olem  26876  basellem4  27411  lgsqrlem2  27674  lgsqrlem3  27675  rpvmasum2  27839  dirith  27856  foresf1o  33100  ofpreima  33259  fnpreimac  33264  1stpreimas  33299  indpreima  33432  s3clhash  33512  pwrssmgc  33561  cycpmconjslem2  33716  cyc3conja  33718  exsslsb  34229  dimkerim  34259  elirng  34318  irngss  34319  irngnzply1  34323  locfinreflem  34472  qqhre  34652  sibfof  34972  cvmliftlem6  36055  cvmliftlem7  36056  cvmliftlem8  36057  cvmliftlem9  36058  taupilem3  38241  itg2addnclem  38590  itg2addnclem2  38591  pw2f1o2val2  44047  dnnumch3  44054  proot1mul  44196  proot1hash  44197  proot1ex  44198  wessf1ornlem  46200  preimafvsnel  48461  uniimaprimaeqfv  48464  elsetpreimafvbi  48473  imasubc  50259  imassc  50261  imaid  50262