Theorem fniniseg 6554

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 6553	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6415	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4379	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 611	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	syl6bb 278	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2155  {csn 4364  ^◡ccnv 5304   “ cima 5308   Fn wfn 6090  ‘cfv 6095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-sbc 3628  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-fv 6103

This theorem is referenced by:  fparlem1  7505  fparlem2  7506  pw2f1olem  8297  recmulnq  10065  dmrecnq  10069  vdwlem1  15896  vdwlem2  15897  vdwlem6  15901  vdwlem8  15903  vdwlem9  15904  vdwlem12  15907  vdwlem13  15908  ramval  15923  ramub1lem1  15941  ghmeqker  17883  efgrelexlemb  18358  efgredeu  18360  psgnevpmb  20134  qtopeu  21727  itg1addlem1  23667  i1faddlem  23668  i1fmullem  23669  i1fmulclem  23677  i1fres  23680  itg10a  23685  itg1ge0a  23686  itg1climres  23689  mbfi1fseqlem4  23693  ply1remlem  24130  ply1rem  24131  fta1glem1  24133  fta1glem2  24134  fta1g  24135  fta1blem  24136  plyco0  24156  ofmulrt  24245  plyremlem  24267  plyrem  24268  fta1lem  24270  fta1  24271  vieta1lem1  24273  vieta1lem2  24274  vieta1  24275  plyexmo  24276  elaa  24279  aannenlem1  24291  aalioulem2  24296  pilem1  24413  efif1olem3  24499  efif1olem4  24500  efifo  24502  eff1olem  24503  basellem4  25018  lgsqrlem2  25280  lgsqrlem3  25281  rpvmasum2  25409  dirith  25426  foresf1o  29662  ofpreima  29786  1stpreimas  29804  locfinreflem  30226  qqhre  30383  indpi1  30401  indpreima  30406  sibfof  30721  cvmliftlem6  31589  cvmliftlem7  31590  cvmliftlem8  31591  cvmliftlem9  31592  taupilem3  33476  itg2addnclem  33767  itg2addnclem2  33768  pw2f1o2val2  38102  dnnumch3  38112  proot1mul  38272  proot1hash  38273  proot1ex  38274  wessf1ornlem  39854