Theorem funeq 6355

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 3949	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6354	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3948	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6354	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 215	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3858  Fun wfun 6329

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-br 5033  df-opab 5095  df-rel 5531  df-cnv 5532  df-co 5533  df-fun 6337

This theorem is referenced by:  funeqi  6356  funeqd  6357  fununi  6410  cnvresid  6414  fneq1  6425  funop  6902  funsndifnop  6904  nvof1o  7029  funcnvuni  7641  fiun  7648  elpmg  8432  fundmeng  8603  isfsupp  8870  dfac9  9596  axdc3lem2  9911  frlmphllem  20545  usgredgop  27062  locfinreflem  31311  orvcval  31943  bnj1379  32330  bnj1385  32332  bnj1497  32560  funen1cnv  32585  oldval  33598  elfunsg  33767  funop1  44207