Theorem fniniseg 7050

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 7048	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6889	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4616	. . 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 4601  ^◡ccnv 5653   “ cima 5657   Fn wfn 6526  ‘cfv 6531

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-fv 6539

This theorem is referenced by:  fparlem1  8111  fparlem2  8112  pw2f1olem  9090  recmulnq  10978  dmrecnq  10982  vdwlem1  17001  vdwlem2  17002  vdwlem6  17006  vdwlem8  17008  vdwlem9  17009  vdwlem12  17012  vdwlem13  17013  ramval  17028  ramub1lem1  17046  ghmeqker  19226  ghmqusnsglem1  19263  ghmquskerlem1  19266  ghmqusker  19270  efgrelexlemb  19731  efgredeu  19733  psgnevpmb  21547  qtopeu  23654  itg1addlem1  25645  i1faddlem  25646  i1fmullem  25647  i1fmulclem  25655  i1fres  25658  itg10a  25663  itg1ge0a  25664  itg1climres  25667  mbfi1fseqlem4  25671  ply1remlem  26122  ply1rem  26123  fta1glem1  26125  fta1glem2  26126  fta1g  26127  fta1blem  26128  plyco0  26149  ofmulrt  26241  plyremlem  26264  plyrem  26265  fta1lem  26267  fta1  26268  vieta1lem1  26270  vieta1lem2  26271  vieta1  26272  plyexmo  26273  elaa  26276  aannenlem1  26288  aalioulem2  26293  pilem1  26413  efif1olem3  26505  efif1olem4  26506  efifo  26508  eff1olem  26509  basellem4  27046  lgsqrlem2  27310  lgsqrlem3  27311  rpvmasum2  27475  dirith  27492  foresf1o  32485  ofpreima  32643  fnpreimac  32649  1stpreimas  32683  indpi1  32837  indpreima  32842  s3clhash  32923  pwrssmgc  32980  cycpmconjslem2  33166  cyc3conja  33168  exsslsb  33636  dimkerim  33667  elirng  33727  irngss  33728  irngnzply1  33732  locfinreflem  33871  qqhre  34051  sibfof  34372  cvmliftlem6  35312  cvmliftlem7  35313  cvmliftlem8  35314  cvmliftlem9  35315  taupilem3  37337  itg2addnclem  37695  itg2addnclem2  37696  pw2f1o2val2  43064  dnnumch3  43071  proot1mul  43218  proot1hash  43219  proot1ex  43220  wessf1ornlem  45209  preimafvsnel  47393  uniimaprimaeqfv  47396  elsetpreimafvbi  47405  imasubc  49091  imassc  49093  imaid  49094