Theorem funeq 6553

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 3990	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6552	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 18	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3989	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6552	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 18	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 215	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3899  Fun wfun 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-fun 6535

This theorem is used by:  funeqi  6554  funeqd  6555  fununi  6609  cnvresid  6613  fneq1  6624  funop  7147  funsndifnop  7149  nvof1o  7282  funcnvuni  7930  fiun  7941  elpmg  8843  funen1cnv  9036  fundmeng  9040  isfsupp  9336  dfac9  10140  axdc3lem2  10454  frlmphllem  21994  psdmul  22395  oldval  28100  usgredgop  29631  locfinreflem  34351  orvcval  34970  bnj1379  35340  bnj1385  35342  bnj1497  35570  elfunsg  36494  modelaxreplem1  45802  modelaxreplem2  45803  modelaxrep  45805  funop1  48172