Theorem funeq 6539

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 4009	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6538	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 4008	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6538	. . 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 1540   ⊆ wss 3917  Fun wfun 6508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-fun 6516

This theorem is referenced by:  funeqi  6540  funeqd  6541  fununi  6594  cnvresid  6598  fneq1  6612  funop  7124  funsndifnop  7126  nvof1o  7258  funcnvuni  7911  fiun  7924  elpmg  8819  fundmeng  9006  isfsupp  9323  dfac9  10097  axdc3lem2  10411  frlmphllem  21696  psdmul  22060  oldval  27769  usgredgop  29104  locfinreflem  33837  orvcval  34456  bnj1379  34827  bnj1385  34829  bnj1497  35057  funen1cnv  35085  elfunsg  35911  modelaxreplem1  44975  modelaxreplem2  44976  modelaxrep  44978  funop1  47288