Theorem f1ocnvfv 7234

Description: Relationship between the value of a one-to-one onto function and the value of its converse. (Contributed by Raph Levien, 10-Apr-2004.)

Assertion

Ref	Expression
f1ocnvfv	⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶))

Proof of Theorem f1ocnvfv

Step	Hyp	Ref	Expression
1		fveq2 6842	. . 3 ⊢ (𝐷 = (𝐹‘𝐶) → (◡𝐹‘𝐷) = (◡𝐹‘(𝐹‘𝐶)))
2	1	eqcoms 2745	. 2 ⊢ ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = (◡𝐹‘(𝐹‘𝐶)))
3		f1ocnvfv1 7232	. . 3 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶)
4	3	eqeq2d 2748	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹‘𝐷) = (◡𝐹‘(𝐹‘𝐶)) ↔ (◡𝐹‘𝐷) = 𝐶))
5	2, 4	imbitrid 244	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) = 𝐷 → (◡𝐹‘𝐷) = 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ^◡ccnv 5631  –1-1-onto→wf1o 6499  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508

This theorem is referenced by:  f1ocnvfvb  7235  f1oiso2  7308  curry1  8056  curry2  8059  dif1en  9098  mapfienlem2  9321  infxpenc2lem1  9941  axcclem  10379  uzrdgfni  13893  uzrdgsuci  13895  fzennn  13903  axdc4uzlem  13918  seqf1olem1  13976  seqf1olem2  13977  hashginv  14269  sadaddlem  16405  xpsaddlem  17506  xpsvsca  17510  xpsle  17512  catcisolem  18046  mgmhmf1o  18637  mhmf1o  18733  ghmf1o  19189  lmhmf1o  21010  symgtgp  24062  xpsdsval  24337  noseqrdgfn  28314  noseqrdgsuc  28316  cnvbraval  32198  madjusmdetlem2  34006  reprpmtf1o  34804  derangenlem  35387  subfacp1lem4  35399  subfacp1lem5  35400  cvmliftlem9  35509  rngoisocnv  38232  cdleme51finvfvN  40931  ltrniotacnvval  40958  dssmapclsntr  44485  isubgr3stgrlem7  48332