Theorem funeq 6559

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 6558	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 18	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3989	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6558	. . 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 6532

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ss 3916  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-fun 6540

This theorem is used by:  funeqi  6560  funeqd  6561  fununi  6615  cnvresid  6619  fneq1  6630  funop  7153  funsndifnop  7155  nvof1o  7288  funcnvuni  7944  fiun  7955  elpmg  8863  funen1cnv  9056  fundmeng  9060  isfsupp  9357  dfac9  10215  axdc3lem2  10529  frlmphllem  22086  psdmul  22487  oldval  28220  usgredgop  29751  locfinreflem  34472  orvcval  35090  bnj1379  35460  bnj1385  35462  bnj1497  35690  elfunsg  36678  modelaxreplem1  45967  modelaxreplem2  45968  modelaxrep  45970  funop1  48352