Theorem funeq 6496

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3916  df-br 5089  df-opab 5151  df-rel 5620  df-cnv 5621  df-co 5622  df-fun 6478

This theorem is referenced by:  funeqi  6497  funeqd  6498  fununi  6551  cnvresid  6555  fneq1  6567  funop  7076  funsndifnop  7078  nvof1o  7208  funcnvuni  7856  fiun  7869  elpmg  8761  fundmeng  8948  isfsupp  9243  dfac9  10019  axdc3lem2  10333  frlmphllem  21671  psdmul  22035  oldval  27749  usgredgop  29102  locfinreflem  33821  orvcval  34439  bnj1379  34810  bnj1385  34812  bnj1497  35040  funen1cnv  35068  elfunsg  35907  modelaxreplem1  44968  modelaxreplem2  44969  modelaxrep  44971  funop1  47281