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  7928  fiun  7939  elpmg  8839  fundmeng  9028  isfsupp  9324  dfac9  10119  axdc3lem2  10434  frlmphllem  21898  psdmul  22297  oldval  27992  usgredgop  29460  locfinreflem  34174  orvcval  34792  bnj1379  35162  bnj1385  35164  bnj1497  35392  funen1cnv  35419  elfunsg  36304  modelaxreplem1  45578  modelaxreplem2  45579  modelaxrep  45581  funop1  47908