Theorem funeq 6567

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ⊆ wss 3899  Fun wfun 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3900  df-br 5106  df-opab 5170  df-rel 5661  df-cnv 5662  df-co 5663  df-fun 6548

This theorem is used by:  funeqi  6568  funeqd  6569  fununi  6623  cnvresid  6627  fneq1  6638  funop  7161  funsndifnop  7163  nvof1o  7295  funcnvuni  7951  fiun  7962  elpmg  8874  funen1cnv  9067  fundmeng  9071  isfsupp  9368  dfac9  10225  axdc3lem2  10539  frlmphllem  22098  psdmul  22499  oldval  28232  usgredgop  29763  locfinreflem  34525  orvcval  35143  bnj1379  35513  bnj1385  35515  bnj1497  35743  srepdflem2  36040  srepdf  36041  elfunsg  36805  modelaxreplem1  46107  modelaxreplem2  46108  modelaxrep  46110  funop1  48492