Theorem f1oeq3d 6839

Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Hypothesis

Ref	Expression
f1oeq3d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
f1oeq3d	⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Proof of Theorem f1oeq3d

Step	Hyp	Ref	Expression
1		f1oeq3d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		f1oeq3 6832	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  –1-1-onto→wf1o 6550

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-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558

This theorem is referenced by:  resdif  6863  f1osng  6883  f1oresrab  7140  fveqf1o  7316  isoini2  7351  oacomf1o  8590  mapsnf1o  8962  domss2  9165  dif1enlem  9185  dif1enlemOLD  9186  infn0  9336  wemapwe  9726  oef1o  9727  cnfcomlem  9728  cnfcom3  9733  cnfcom3clem  9734  infxpenc  10047  infxpenc2lem1  10048  infxpenc2  10051  ackbij2lem2  10269  hsmexlem1  10455  fsumss  15709  fsumcnv  15757  fprodss  15930  fprodcnv  15965  pwssnf1o  17485  catcisolem  18104  equivestrcsetc  18148  yoniso  18282  gsumpropd  18643  gsumpropd2lem  18644  xpsmnd  18739  xpsgrp  19020  ghmqusker  19243  gsumval3lem1  19865  gsumval3lem2  19866  gsumcom2  19935  xpsrngd  20124  xpsringd  20273  rngqiprngim  21199  coe1mul2lem2  22192  scmatrngiso  22456  m2cpmrngiso  22678  cncfcnvcn  24864  isismt  28356  usgrf1oedg  29038  wlkiswwlks2lem5  29702  clwwlkvbij  29941  eupthres  30043  eupthp1  30044  cycpmconjvlem  32880  tocyccntz  32883  idomsubr  33013  dimkerim  33330  poimirlem4  37102  poimirlem9  37107  rngoisoval  37455  frlmsnic  41773  sge0f1o  45772  nnfoctbdj  45846  f1oresf1o  46672  grimidvtxedg  47225  ushggricedg  47244

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »