Theorem funeq 6344

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 3972	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6343	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3971	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6343	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 215	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3881  Fun wfun 6318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-fun 6326

This theorem is referenced by:  funeqi  6345  funeqd  6346  fununi  6399  cnvresid  6403  fneq1  6414  funop  6888  funsndifnop  6890  nvof1o  7015  funcnvuni  7618  fiun  7626  elpmg  8405  fundmeng  8567  isfsupp  8821  dfac9  9547  axdc3lem2  9862  frlmphllem  20469  usgredgop  26963  locfinreflem  31193  orvcval  31825  bnj1379  32212  bnj1385  32214  bnj1497  32442  funen1cnv  32467  elfunsg  33490  funop1  43839