Theorem funeq 6505

Description: Equality theorem for function predicate. (Contributed by NM, 16-Aug-1994.)

Assertion

Ref	Expression
funeq	⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Proof of Theorem funeq

Step	Hyp	Ref	Expression
1		eqimss2 3974	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6504	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3973	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6504	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 213	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ⊆ wss 3883  Fun wfun 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900  df-br 5073  df-opab 5135  df-rel 5625  df-cnv 5626  df-co 5627  df-fun 6487

This theorem is referenced by:  funeqi  6506  funeqd  6507  fununi  6560  cnvresid  6564  fneq1  6576  funop  7092  funsndifnop  7094  nvof1o  7224  funcnvuni  7872  fiun  7885  elpmg  8780  fundmeng  8969  isfsupp  9268  dfac9  10050  axdc3lem2  10364  frlmphllem  21755  psdmul  22154  oldval  27844  usgredgop  29257  locfinreflem  34024  orvcval  34642  bnj1379  35012  bnj1385  35014  bnj1497  35242  funen1cnv  35269  elfunsg  36142  modelaxreplem1  45422  modelaxreplem2  45423  modelaxrep  45425  funop1  47746