Theorem funeq 6560

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 3997	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6559	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 18	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3996	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6559	. . 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 3906  Fun wfun 6534

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-fun 6542

This theorem is used by:  funeqi  6561  funeqd  6562  fununi  6615  cnvresid  6619  fneq1  6630  funop  7152  funsndifnop  7154  nvof1o  7287  funcnvuni  7935  fiun  7946  elpmg  8846  funen1cnv  9032  fundmeng  9036  isfsupp  9332  dfac9  10136  axdc3lem2  10450  frlmphllem  21982  psdmul  22381  oldval  28080  usgredgop  29580  locfinreflem  34296  orvcval  34915  bnj1379  35285  bnj1385  35287  bnj1497  35515  elfunsg  36445  modelaxreplem1  45747  modelaxreplem2  45748  modelaxrep  45750  funop1  48080