Theorem funeqi 6370

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 6369	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (Fun 𝐴 ↔ Fun 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1533  Fun wfun 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951  df-br 5059  df-opab 5121  df-rel 5556  df-cnv 5557  df-co 5558  df-fun 6351

This theorem is referenced by:  funmpt  6387  funmpt2  6388  funco  6389  funresfunco  6390  fununfun  6396  funprg  6402  funtpg  6403  funtp  6405  funcnvpr  6410  funcnvtp  6411  funcnvqp  6412  funcnv0  6414  f1cnvcnv  6578  f1co  6579  opabiotafun  6738  fvn0ssdmfun  6836  funopdmsn  6906  fpropnf1  7019  funoprabg  7267  mpofun  7270  ovidig  7286  funcnvuni  7630  fiun  7638  f1iun  7639  tposfun  7902  tfr1a  8024  tz7.44lem1  8035  tz7.48-2  8072  ssdomg  8549  sbthlem7  8627  sbthlem8  8628  1sdom  8715  hartogslem1  9000  r1funlim  9189  zorn2lem4  9915  axaddf  10561  axmulf  10562  fundmge2nop0  13844  funcnvs1  14268  strleun  16585  fthoppc  17187  cnfldfun  20551  cnfldfunALT  20552  volf  24124  dfrelog  25143  usgredg3  26992  ushgredgedg  27005  ushgredgedgloop  27007  2trld  27711  0pth  27898  1pthdlem1  27908  1trld  27915  3trld  27945  ajfuni  28630  hlimf  29008  funadj  29657  funcnvadj  29664  rinvf1o  30369  bnj97  32133  bnj150  32143  bnj1384  32299  bnj1421  32309  bnj60  32329  satffunlem2lem2  32648  satfv0fvfmla0  32655  funpartfun  33399  funtransport  33487  funray  33596  funline  33598  bj-isrvec  34569  xlimfun  42129  funcoressn  43271