Theorem fniniseg 7091

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 7088	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6929	. . . 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 2147  {csn 4588  ^◡ccnv 5657   “ cima 5661   Fn wfn 6561  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574

This theorem is used by:  fparlem1  8160  fparlem2  8161  pw2f1olem  9138  recmulnq  11088  dmrecnq  11092  indpi1  12374  vdwlem1  17203  vdwlem2  17204  vdwlem6  17208  vdwlem8  17210  vdwlem9  17211  vdwlem12  17214  vdwlem13  17215  ramval  17230  ramub1lem1  17248  ghmeqker  19507  ghmqusnsglem1  19545  ghmquskerlem1  19548  ghmqusker  19552  efgrelexlemb  20015  efgredeu  20017  psgnevpmb  21948  qtopeu  24090  itg1addlem1  26068  i1faddlem  26069  i1fmullem  26070  i1fmulclem  26078  i1fres  26081  itg10a  26086  itg1ge0a  26087  itg1climres  26090  mbfi1fseqlem4  26094  ply1remlem  26538  ply1rem  26539  fta1glem1  26541  fta1glem2  26542  fta1g  26543  fta1blem  26544  plyco0  26565  ofmulrt  26655  plyremlem  26680  plyrem  26681  fta1lem  26683  fta1  26684  rnplynfin  26685  plyconz  26686  vieta1lem1  26688  vieta1lem2  26689  vieta1  26690  plyexmo  26691  elaa  26696  aannenlem1  26712  aalioulem2  26717  pilem1  26835  efif1olem3  26929  efif1olem4  26930  efifo  26932  eff1olem  26933  basellem4  27468  lgsqrlem2  27731  lgsqrlem3  27732  rpvmasum2  27896  dirith  27913  foresf1o  33199  ofpreima  33357  fnpreimac  33362  1stpreimas  33396  indpreima  33528  s3clhash  33608  pwrssmgc  33660  cycpmconjslem2  33815  cyc3conja  33817  exsslsb  34340  dimkerim  34370  elirng  34429  irngss  34430  irngnzply1  34434  locfinreflem  34583  qqhre  34763  sibfof  35083  cvmliftlem6  36263  cvmliftlem7  36264  cvmliftlem8  36265  cvmliftlem9  36266  taupilem3  38508  itg2addnclem  38857  itg2addnclem2  38858  pw2f1o2val2  44313  dnnumch3  44320  proot1mul  44457  proot1hash  44458  proot1ex  44459  wessf1ornlem  46473  preimafvsnel  48734  uniimaprimaeqfv  48737  elsetpreimafvbi  48746  imasubc  50598  imassc  50600  imaid  50601