Theorem funeq 6510

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 3991	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6509	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3990	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6509	. . 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 1541   ⊆ wss 3899  Fun wfun 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916  df-br 5097  df-opab 5159  df-rel 5629  df-cnv 5630  df-co 5631  df-fun 6492

This theorem is referenced by:  funeqi  6511  funeqd  6512  fununi  6565  cnvresid  6569  fneq1  6581  funop  7092  funsndifnop  7094  nvof1o  7224  funcnvuni  7872  fiun  7885  elpmg  8778  fundmeng  8967  isfsupp  9266  dfac9  10045  axdc3lem2  10359  frlmphllem  21733  psdmul  22107  oldval  27822  usgredgop  29192  locfinreflem  33946  orvcval  34564  bnj1379  34935  bnj1385  34937  bnj1497  35165  funen1cnv  35193  elfunsg  36057  modelaxreplem1  45161  modelaxreplem2  45162  modelaxrep  45164  funop1  47471