Theorem fniniseg 6294

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 6293	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6158	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4163	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 729	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	syl6bb 276	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  {csn 4148  ^◡ccnv 5073   “ cima 5077   Fn wfn 5842  ‘cfv 5847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-fv 5855

This theorem is referenced by:  fparlem1  7222  fparlem2  7223  pw2f1olem  8008  recmulnq  9730  dmrecnq  9734  vdwlem1  15609  vdwlem2  15610  vdwlem6  15614  vdwlem8  15616  vdwlem9  15617  vdwlem12  15620  vdwlem13  15621  ramval  15636  ramub1lem1  15654  ghmeqker  17608  efgrelexlemb  18084  efgredeu  18086  psgnevpmb  19852  qtopeu  21429  itg1addlem1  23365  i1faddlem  23366  i1fmullem  23367  i1fmulclem  23375  i1fres  23378  itg10a  23383  itg1ge0a  23384  itg1climres  23387  mbfi1fseqlem4  23391  ply1remlem  23826  ply1rem  23827  fta1glem1  23829  fta1glem2  23830  fta1g  23831  fta1blem  23832  plyco0  23852  ofmulrt  23941  plyremlem  23963  plyrem  23964  fta1lem  23966  fta1  23967  vieta1lem1  23969  vieta1lem2  23970  vieta1  23971  plyexmo  23972  elaa  23975  aannenlem1  23987  aalioulem2  23992  pilem1  24109  efif1olem3  24194  efif1olem4  24195  efifo  24197  eff1olem  24198  basellem4  24710  lgsqrlem2  24972  lgsqrlem3  24973  rpvmasum2  25101  dirith  25118  foresf1o  29187  ofpreima  29305  1stpreimas  29323  locfinreflem  29686  qqhre  29843  indpi1  29862  indpreima  29865  sibfof  30180  cvmliftlem6  30977  cvmliftlem7  30978  cvmliftlem8  30979  cvmliftlem9  30980  taupilem3  32795  itg2addnclem  33090  itg2addnclem2  33091  pw2f1o2val2  37084  dnnumch3  37094  proot1mul  37255  proot1hash  37256  proot1ex  37257  wessf1ornlem  38842