Theorem fniniseg 7032

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {csn 4589  ^◡ccnv 5637   “ cima 5641   Fn wfn 6506  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  fparlem1  8091  fparlem2  8092  pw2f1olem  9045  recmulnq  10917  dmrecnq  10921  vdwlem1  16952  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem12  16963  vdwlem13  16964  ramval  16979  ramub1lem1  16997  ghmeqker  19175  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmqusker  19219  efgrelexlemb  19680  efgredeu  19682  psgnevpmb  21496  qtopeu  23603  itg1addlem1  25593  i1faddlem  25594  i1fmullem  25595  i1fmulclem  25603  i1fres  25606  itg10a  25611  itg1ge0a  25612  itg1climres  25615  mbfi1fseqlem4  25619  ply1remlem  26070  ply1rem  26071  fta1glem1  26073  fta1glem2  26074  fta1g  26075  fta1blem  26076  plyco0  26097  ofmulrt  26189  plyremlem  26212  plyrem  26213  fta1lem  26215  fta1  26216  vieta1lem1  26218  vieta1lem2  26219  vieta1  26220  plyexmo  26221  elaa  26224  aannenlem1  26236  aalioulem2  26241  pilem1  26361  efif1olem3  26453  efif1olem4  26454  efifo  26456  eff1olem  26457  basellem4  26994  lgsqrlem2  27258  lgsqrlem3  27259  rpvmasum2  27423  dirith  27440  foresf1o  32433  ofpreima  32589  fnpreimac  32595  1stpreimas  32629  indpi1  32783  indpreima  32788  s3clhash  32869  pwrssmgc  32926  cycpmconjslem2  33112  cyc3conja  33114  exsslsb  33592  dimkerim  33623  elirng  33681  irngss  33682  irngnzply1  33686  locfinreflem  33830  qqhre  34010  sibfof  34331  cvmliftlem6  35277  cvmliftlem7  35278  cvmliftlem8  35279  cvmliftlem9  35280  taupilem3  37307  itg2addnclem  37665  itg2addnclem2  37666  pw2f1o2val2  43029  dnnumch3  43036  proot1mul  43183  proot1hash  43184  proot1ex  43185  wessf1ornlem  45179  preimafvsnel  47380  uniimaprimaeqfv  47383  elsetpreimafvbi  47392  imasubc  49140  imassc  49142  imaid  49143