Theorem fniniseg 7052

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 7050	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6891	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4599	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 635	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	bitrdi 290	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {csn 4584  ^◡ccnv 5654   “ cima 5658   Fn wfn 6528  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  fparlem1  8109  fparlem2  8110  pw2f1olem  9079  recmulnq  10973  dmrecnq  10977  indpi1  12256  vdwlem1  17073  vdwlem2  17074  vdwlem6  17078  vdwlem8  17080  vdwlem9  17081  vdwlem12  17084  vdwlem13  17085  ramval  17100  ramub1lem1  17118  ghmeqker  19370  ghmqusnsglem1  19407  ghmquskerlem1  19410  ghmqusker  19414  efgrelexlemb  19877  efgredeu  19879  psgnevpmb  21800  qtopeu  23942  itg1addlem1  25920  i1faddlem  25921  i1fmullem  25922  i1fmulclem  25930  i1fres  25933  itg10a  25938  itg1ge0a  25939  itg1climres  25942  mbfi1fseqlem4  25946  ply1remlem  26390  ply1rem  26391  fta1glem1  26393  fta1glem2  26394  fta1g  26395  fta1blem  26396  plyco0  26417  ofmulrt  26509  plyremlem  26534  plyrem  26535  fta1lem  26537  fta1  26538  rnplynfin  26539  plyconz  26540  vieta1lem1  26542  vieta1lem2  26543  vieta1  26544  plyexmo  26545  elaa  26548  aannenlem1  26564  aalioulem2  26569  pilem1  26687  efif1olem3  26781  efif1olem4  26782  efifo  26784  eff1olem  26785  basellem4  27320  lgsqrlem2  27583  lgsqrlem3  27584  rpvmasum2  27748  dirith  27765  foresf1o  32979  ofpreima  33138  fnpreimac  33143  1stpreimas  33178  indpreima  33311  s3clhash  33391  pwrssmgc  33440  cycpmconjslem2  33595  cyc3conja  33597  exsslsb  34107  dimkerim  34137  elirng  34196  irngss  34197  irngnzply1  34201  locfinreflem  34350  qqhre  34530  sibfof  34851  cvmliftlem6  35869  cvmliftlem7  35870  cvmliftlem8  35871  cvmliftlem9  35872  taupilem3  38071  itg2addnclem  38420  itg2addnclem2  38421  pw2f1o2val2  43881  dnnumch3  43888  proot1mul  44035  proot1hash  44036  proot1ex  44037  wessf1ornlem  46017  preimafvsnel  48279  uniimaprimaeqfv  48282  elsetpreimafvbi  48291  imasubc  50077  imassc  50079  imaid  50080