Theorem funeqi 5345

Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
funeqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
funeqi	⊢ (Fun 𝐴 ↔ Fun 𝐵)

Proof of Theorem funeqi

Step	Hyp	Ref	Expression
1		funeqi.1	. 2 ⊢ 𝐴 = 𝐵
2		funeq 5344	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐴 ↔ Fun 𝐵)

Syntax hints:   ↔ wb 105   = wceq 1395  Fun wfun 5318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3204  df-ss 3211  df-br 4087  df-opab 4149  df-rel 4730  df-cnv 4731  df-co 4732  df-fun 5326

This theorem is referenced by:  funmpt  5362  funmpt2  5363  fununfun  5370  funprg  5377  funtpg  5378  funtp  5380  funcnvuni  5396  f1cnvcnv  5550  f1co  5551  fun11iun  5601  f10  5614  funopdmsn  5829  funoprabg  6115  mpofun  6118  ovidig  6134  tposfun  6421  tfri1dALT  6512  tfrcl  6525  rdgfun  6534  frecfun  6556  frecfcllem  6565  th3qcor  6803  ssdomg  6947  sbthlem7  7153  sbthlemi8  7154  casefun  7275  caseinj  7279  djufun  7294  djuinj  7296  ctssdccl  7301  axaddf  8078  axmulf  8079  fundm2domnop0  11099  strleund  13176  strleun  13177  1strbas  13190  2strbasg  13193  2stropg  13194  lidlmex  14479  usgredg3  16053  ushgredgedg  16065  ushgredgedgloop  16067