Theorem funeq 6536

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 4006	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6535	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 4005	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6535	. . 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 1540   ⊆ wss 3914  Fun wfun 6505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-fun 6513

This theorem is referenced by:  funeqi  6537  funeqd  6538  fununi  6591  cnvresid  6595  fneq1  6609  funop  7121  funsndifnop  7123  nvof1o  7255  funcnvuni  7908  fiun  7921  elpmg  8816  fundmeng  9003  isfsupp  9316  dfac9  10090  axdc3lem2  10404  frlmphllem  21689  psdmul  22053  oldval  27762  usgredgop  29097  locfinreflem  33830  orvcval  34449  bnj1379  34820  bnj1385  34822  bnj1497  35050  funen1cnv  35078  elfunsg  35904  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  funop1  47284