Theorem funeq 6541

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 3995	. . 3 ⊢ (𝐴 = 𝐵 → 𝐵 ⊆ 𝐴)
2		funss 6540	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (Fun 𝐴 → Fun 𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 → Fun 𝐵))
4		eqimss 3994	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
5		funss 6540	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))
6	4, 5	syl 17	. 2 ⊢ (𝐴 = 𝐵 → (Fun 𝐵 → Fun 𝐴))
7	3, 6	impbid 214	1 ⊢ (𝐴 = 𝐵 → (Fun 𝐴 ↔ Fun 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ⊆ wss 3904  Fun wfun 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921  df-br 5101  df-opab 5163  df-rel 5654  df-cnv 5655  df-co 5656  df-fun 6523

This theorem is referenced by:  funeqi  6542  funeqd  6543  fununi  6596  cnvresid  6600  fneq1  6612  funop  7132  funsndifnop  7134  nvof1o  7264  funcnvuni  7913  fiun  7924  elpmg  8824  fundmeng  9013  isfsupp  9311  dfac9  10093  axdc3lem2  10408  frlmphllem  21832  psdmul  22231  oldval  27927  usgredgop  29371  locfinreflem  34137  orvcval  34755  bnj1379  35125  bnj1385  35127  bnj1497  35355  funen1cnv  35382  elfunsg  36264  modelaxreplem1  45554  modelaxreplem2  45555  modelaxrep  45557  funop1  47877