MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1oeq1d Structured version   Visualization version   GIF version

Theorem f1oeq1d 6780
Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
f1oeq1d.1 (𝜑𝐹 = 𝐺)
Assertion
Ref Expression
f1oeq1d (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))

Proof of Theorem f1oeq1d
StepHypRef Expression
1 f1oeq1d.1 . 2 (𝜑𝐹 = 𝐺)
2 f1oeq1 6773 . 2 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  1-1-ontowf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  f1orescnv  6800  f1osng  6826  f1ofvswap  7253  dif1en  9105  dif1enOLD  9107  cnfcomlem  9636  cnfcom2  9639  cnfcom3clem  9642  infxpenc  9955  infxpenc2lem2  9957  infxpenc2  9959  canthp1lem2  10590  pwfseqlem5  10600  pwfseq  10601  s2f1o  14806  s4f1o  14808  bitsf1ocnv  16325  yonffthlem  18172  grplactcnv  18851  eqgen  18984  znunithash  20974  tgpconncompeqg  23466  fcobijfs  31643  s2f1  31804  mgcf1o  31866  gsummpt2d  31894  indf1o  32626  subfacp1lem3  33779  subfacp1lem5  33781  ismrer1  36300  hvmap1o  40229  metakunt34  40613
  Copyright terms: Public domain W3C validator