Theorem funeq 6454

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 3978	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6453	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3977	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6453	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 211	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ⊆ wss 3887  Fun wfun 6427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-fun 6435

This theorem is referenced by:  funeqi  6455  funeqd  6456  fununi  6509  cnvresid  6513  fneq1  6524  funop  7021  funsndifnop  7023  nvof1o  7152  funcnvuni  7778  fiun  7785  elpmg  8631  fundmeng  8822  isfsupp  9132  dfac9  9892  axdc3lem2  10207  frlmphllem  20987  usgredgop  27540  locfinreflem  31790  orvcval  32424  bnj1379  32810  bnj1385  32812  bnj1497  33040  funen1cnv  33060  oldval  34038  elfunsg  34218  funop1  44775