Theorem funeq 6513

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 3982	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6512	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3981	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6512	. . 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 3890  Fun wfun 6487

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-rel 5632  df-cnv 5633  df-co 5634  df-fun 6495

This theorem is referenced by:  funeqi  6514  funeqd  6515  fununi  6568  cnvresid  6572  fneq1  6584  funop  7097  funsndifnop  7099  nvof1o  7229  funcnvuni  7877  fiun  7890  elpmg  8784  fundmeng  8973  isfsupp  9272  dfac9  10053  axdc3lem2  10367  frlmphllem  21773  psdmul  22145  oldval  27843  usgredgop  29256  locfinreflem  34003  orvcval  34621  bnj1379  34991  bnj1385  34993  bnj1497  35221  funen1cnv  35250  elfunsg  36115  modelaxreplem1  45426  modelaxreplem2  45427  modelaxrep  45429  funop1  47746