Theorem funeq 6556

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3905  Fun wfun 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3922  df-br 5110  df-opab 5174  df-rel 5668  df-cnv 5669  df-co 5670  df-fun 6538

This theorem is referenced by:  funeqi  6557  funeqd  6558  fununi  6611  cnvresid  6615  fneq1  6626  funop  7146  funsndifnop  7148  nvof1o  7278  funcnvuni  7925  fiun  7936  elpmg  8836  fundmeng  9025  isfsupp  9321  dfac9  10116  axdc3lem2  10430  frlmphllem  21930  psdmul  22329  oldval  28027  usgredgop  29520  locfinreflem  34230  orvcval  34848  bnj1379  35218  bnj1385  35220  bnj1497  35448  funen1cnv  35477  elfunsg  36406  modelaxreplem1  45687  modelaxreplem2  45688  modelaxrep  45690  funop1  48020