Theorem funeq 6518

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 3981	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6517	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3980	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6517	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 212	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3889  Fun wfun 6492

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-fun 6500

This theorem is referenced by:  funeqi  6519  funeqd  6520  fununi  6573  cnvresid  6577  fneq1  6589  funop  7103  funsndifnop  7105  nvof1o  7235  funcnvuni  7883  fiun  7896  elpmg  8790  fundmeng  8979  isfsupp  9278  dfac9  10059  axdc3lem2  10373  frlmphllem  21760  psdmul  22132  oldval  27826  usgredgop  29239  locfinreflem  33984  orvcval  34602  bnj1379  34972  bnj1385  34974  bnj1497  35202  funen1cnv  35231  elfunsg  36096  modelaxreplem1  45405  modelaxreplem2  45406  modelaxrep  45408  funop1  47731