Theorem fniniseg 6481

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1630   ∈ wcel 2144  {csn 4314  ^◡ccnv 5248   “ cima 5252   Fn wfn 6026  ‘cfv 6031

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-ne 2943  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-uni 4573  df-br 4785  df-opab 4845  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-fv 6039

This theorem is referenced by:  fparlem1  7427  fparlem2  7428  pw2f1olem  8219  recmulnq  9987  dmrecnq  9991  vdwlem1  15891  vdwlem2  15892  vdwlem6  15896  vdwlem8  15898  vdwlem9  15899  vdwlem12  15902  vdwlem13  15903  ramval  15918  ramub1lem1  15936  ghmeqker  17894  efgrelexlemb  18369  efgredeu  18371  psgnevpmb  20147  qtopeu  21739  itg1addlem1  23678  i1faddlem  23679  i1fmullem  23680  i1fmulclem  23688  i1fres  23691  itg10a  23696  itg1ge0a  23697  itg1climres  23700  mbfi1fseqlem4  23704  ply1remlem  24141  ply1rem  24142  fta1glem1  24144  fta1glem2  24145  fta1g  24146  fta1blem  24147  plyco0  24167  ofmulrt  24256  plyremlem  24278  plyrem  24279  fta1lem  24281  fta1  24282  vieta1lem1  24284  vieta1lem2  24285  vieta1  24286  plyexmo  24287  elaa  24290  aannenlem1  24302  aalioulem2  24307  pilem1  24424  efif1olem3  24510  efif1olem4  24511  efifo  24513  eff1olem  24514  basellem4  25030  lgsqrlem2  25292  lgsqrlem3  25293  rpvmasum2  25421  dirith  25438  foresf1o  29675  ofpreima  29799  1stpreimas  29817  locfinreflem  30241  qqhre  30398  indpi1  30416  indpreima  30421  sibfof  30736  cvmliftlem6  31604  cvmliftlem7  31605  cvmliftlem8  31606  cvmliftlem9  31607  taupilem3  33495  itg2addnclem  33786  itg2addnclem2  33787  pw2f1o2val2  38126  dnnumch3  38136  proot1mul  38296  proot1hash  38297  proot1ex  38298  wessf1ornlem  39885