Theorem funeq 6557

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 4004	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6556	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 18	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 4003	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6556	. . 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 1567   ⊆ wss 3913  Fun wfun 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930  df-br 5114  df-opab 5178  df-rel 5669  df-cnv 5670  df-co 5671  df-fun 6539

This theorem is referenced by:  funeqi  6558  funeqd  6559  fununi  6612  cnvresid  6616  fneq1  6627  funop  7147  funsndifnop  7149  nvof1o  7279  funcnvuni  7929  fiun  7940  elpmg  8840  fundmeng  9029  isfsupp  9325  dfac9  10120  axdc3lem2  10435  frlmphllem  21899  psdmul  22298  oldval  27993  usgredgop  29461  locfinreflem  34175  orvcval  34793  bnj1379  35163  bnj1385  35165  bnj1497  35393  funen1cnv  35420  elfunsg  36339  modelaxreplem1  45613  modelaxreplem2  45614  modelaxrep  45616  funop1  47943