Theorem fniniseg 7072

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  {csn 4632  ^◡ccnv 5680   “ cima 5684   Fn wfn 6548  ‘cfv 6553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-fv 6561

This theorem is referenced by:  fparlem1  8125  fparlem2  8126  pw2f1olem  9113  recmulnq  11003  dmrecnq  11007  vdwlem1  16978  vdwlem2  16979  vdwlem6  16983  vdwlem8  16985  vdwlem9  16986  vdwlem12  16989  vdwlem13  16990  ramval  17005  ramub1lem1  17023  ghmeqker  19232  ghmqusnsglem1  19269  ghmquskerlem1  19272  ghmqusker  19276  efgrelexlemb  19743  efgredeu  19745  psgnevpmb  21575  qtopeu  23703  itg1addlem1  25704  i1faddlem  25705  i1fmullem  25706  i1fmulclem  25715  i1fres  25718  itg10a  25723  itg1ge0a  25724  itg1climres  25727  mbfi1fseqlem4  25731  ply1remlem  26184  ply1rem  26185  fta1glem1  26187  fta1glem2  26188  fta1g  26189  fta1blem  26190  plyco0  26211  ofmulrt  26301  plyremlem  26324  plyrem  26325  fta1lem  26327  fta1  26328  vieta1lem1  26330  vieta1lem2  26331  vieta1  26332  plyexmo  26333  elaa  26336  aannenlem1  26348  aalioulem2  26353  pilem1  26473  efif1olem3  26563  efif1olem4  26564  efifo  26566  eff1olem  26567  basellem4  27104  lgsqrlem2  27368  lgsqrlem3  27369  rpvmasum2  27533  dirith  27550  foresf1o  32421  ofpreima  32573  fnpreimac  32579  1stpreimas  32608  s3clhash  32800  pwrssmgc  32858  cycpmconjslem2  33010  cyc3conja  33012  dimkerim  33494  elirng  33533  irngss  33534  irngnzply1  33538  locfinreflem  33611  qqhre  33791  indpi1  33809  indpreima  33814  sibfof  34130  cvmliftlem6  35070  cvmliftlem7  35071  cvmliftlem8  35072  cvmliftlem9  35073  taupilem3  36974  itg2addnclem  37320  itg2addnclem2  37321  pw2f1o2val2  42635  dnnumch3  42645  proot1mul  42796  proot1hash  42797  proot1ex  42798  wessf1ornlem  44729  preimafvsnel  46888  uniimaprimaeqfv  46891  elsetpreimafvbi  46900