Theorem fniniseg 6993

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 6991	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6838	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4588	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 623	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 286	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  {csn 4573  ^◡ccnv 5619   “ cima 5623   Fn wfn 6474  ‘cfv 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fn 6482  df-fv 6487

This theorem is referenced by:  fparlem1  8020  fparlem2  8021  pw2f1olem  8941  recmulnq  10821  dmrecnq  10825  vdwlem1  16779  vdwlem2  16780  vdwlem6  16784  vdwlem8  16786  vdwlem9  16787  vdwlem12  16790  vdwlem13  16791  ramval  16806  ramub1lem1  16824  ghmeqker  18957  efgrelexlemb  19451  efgredeu  19453  psgnevpmb  20898  qtopeu  22973  itg1addlem1  24962  i1faddlem  24963  i1fmullem  24964  i1fmulclem  24973  i1fres  24976  itg10a  24981  itg1ge0a  24982  itg1climres  24985  mbfi1fseqlem4  24989  ply1remlem  25433  ply1rem  25434  fta1glem1  25436  fta1glem2  25437  fta1g  25438  fta1blem  25439  plyco0  25459  ofmulrt  25548  plyremlem  25570  plyrem  25571  fta1lem  25573  fta1  25574  vieta1lem1  25576  vieta1lem2  25577  vieta1  25578  plyexmo  25579  elaa  25582  aannenlem1  25594  aalioulem2  25599  pilem1  25716  efif1olem3  25806  efif1olem4  25807  efifo  25809  eff1olem  25810  basellem4  26339  lgsqrlem2  26601  lgsqrlem3  26602  rpvmasum2  26766  dirith  26783  foresf1o  31138  ofpreima  31289  fnpreimac  31295  1stpreimas  31325  s3clhash  31509  pwrssmgc  31565  cycpmconjslem2  31709  cyc3conja  31711  dimkerim  32006  locfinreflem  32088  qqhre  32268  indpi1  32286  indpreima  32291  sibfof  32607  cvmliftlem6  33551  cvmliftlem7  33552  cvmliftlem8  33553  cvmliftlem9  33554  taupilem3  35603  itg2addnclem  35941  itg2addnclem2  35942  pw2f1o2val2  41133  dnnumch3  41143  proot1mul  41295  proot1hash  41296  proot1ex  41297  wessf1ornlem  43058  preimafvsnel  45191  uniimaprimaeqfv  45194  elsetpreimafvbi  45203