Theorem fniniseg 7080

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {csn 4626  ^◡ccnv 5684   “ cima 5688   Fn wfn 6556  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569

This theorem is referenced by:  fparlem1  8137  fparlem2  8138  pw2f1olem  9116  recmulnq  11004  dmrecnq  11008  vdwlem1  17019  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwlem12  17030  vdwlem13  17031  ramval  17046  ramub1lem1  17064  ghmeqker  19261  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmqusker  19305  efgrelexlemb  19768  efgredeu  19770  psgnevpmb  21605  qtopeu  23724  itg1addlem1  25727  i1faddlem  25728  i1fmullem  25729  i1fmulclem  25737  i1fres  25740  itg10a  25745  itg1ge0a  25746  itg1climres  25749  mbfi1fseqlem4  25753  ply1remlem  26204  ply1rem  26205  fta1glem1  26207  fta1glem2  26208  fta1g  26209  fta1blem  26210  plyco0  26231  ofmulrt  26323  plyremlem  26346  plyrem  26347  fta1lem  26349  fta1  26350  vieta1lem1  26352  vieta1lem2  26353  vieta1  26354  plyexmo  26355  elaa  26358  aannenlem1  26370  aalioulem2  26375  pilem1  26495  efif1olem3  26586  efif1olem4  26587  efifo  26589  eff1olem  26590  basellem4  27127  lgsqrlem2  27391  lgsqrlem3  27392  rpvmasum2  27556  dirith  27573  foresf1o  32523  ofpreima  32675  fnpreimac  32681  1stpreimas  32715  indpi1  32845  indpreima  32850  s3clhash  32932  pwrssmgc  32990  cycpmconjslem2  33175  cyc3conja  33177  exsslsb  33647  dimkerim  33678  elirng  33736  irngss  33737  irngnzply1  33741  locfinreflem  33839  qqhre  34021  sibfof  34342  cvmliftlem6  35295  cvmliftlem7  35296  cvmliftlem8  35297  cvmliftlem9  35298  taupilem3  37320  itg2addnclem  37678  itg2addnclem2  37679  pw2f1o2val2  43052  dnnumch3  43059  proot1mul  43206  proot1hash  43207  proot1ex  43208  wessf1ornlem  45190  preimafvsnel  47366  uniimaprimaeqfv  47369  elsetpreimafvbi  47378