Theorem fniniseg 6830

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 6828	. 2 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵})))
2		fvex 6683	. . . 4 ⊢ (𝐹‘𝐶) ∈ V
3	2	elsn 4582	. . 3 ⊢ ((𝐹‘𝐶) ∈ {𝐵} ↔ (𝐹‘𝐶) = 𝐵)
4	3	anbi2i 624	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) ∈ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵))
5	1, 4	syl6bb 289	1 ⊢ (𝐹 Fn 𝐴 → (𝐶 ∈ (◡𝐹 “ {𝐵}) ↔ (𝐶 ∈ 𝐴 ∧ (𝐹‘𝐶) = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {csn 4567  ^◡ccnv 5554   “ cima 5558   Fn wfn 6350  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-fv 6363

This theorem is referenced by:  fparlem1  7807  fparlem2  7808  pw2f1olem  8621  recmulnq  10386  dmrecnq  10390  vdwlem1  16317  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  vdwlem12  16328  vdwlem13  16329  ramval  16344  ramub1lem1  16362  ghmeqker  18385  efgrelexlemb  18876  efgredeu  18878  psgnevpmb  20731  qtopeu  22324  itg1addlem1  24293  i1faddlem  24294  i1fmullem  24295  i1fmulclem  24303  i1fres  24306  itg10a  24311  itg1ge0a  24312  itg1climres  24315  mbfi1fseqlem4  24319  ply1remlem  24756  ply1rem  24757  fta1glem1  24759  fta1glem2  24760  fta1g  24761  fta1blem  24762  plyco0  24782  ofmulrt  24871  plyremlem  24893  plyrem  24894  fta1lem  24896  fta1  24897  vieta1lem1  24899  vieta1lem2  24900  vieta1  24901  plyexmo  24902  elaa  24905  aannenlem1  24917  aalioulem2  24922  pilem1  25039  efif1olem3  25128  efif1olem4  25129  efifo  25131  eff1olem  25132  basellem4  25661  lgsqrlem2  25923  lgsqrlem3  25924  rpvmasum2  26088  dirith  26105  foresf1o  30265  ofpreima  30410  fnpreimac  30416  1stpreimas  30441  s3clhash  30624  cycpmconjslem2  30797  cyc3conja  30799  dimkerim  31023  locfinreflem  31104  qqhre  31261  indpi1  31279  indpreima  31284  sibfof  31598  cvmliftlem6  32537  cvmliftlem7  32538  cvmliftlem8  32539  cvmliftlem9  32540  taupilem3  34603  itg2addnclem  34958  itg2addnclem2  34959  pw2f1o2val2  39657  dnnumch3  39667  proot1mul  39819  proot1hash  39820  proot1ex  39821  wessf1ornlem  41465  preimafvsnel  43559  uniimaprimaeqfv  43562  elsetpreimafvbi  43571