Theorem funeq 4544

Description: Equality theorem for function predicate.

Assertion

Ref	Expression
funeq	|- (A = B -> (Fun A <-> Fun B))

Proof of Theorem funeq

Step	Hyp	Ref	Expression
1		funss 4543	. . . 4 |- (B C_ A -> (Fun A -> Fun B))
2		funss 4543	. . . 4 |- (A C_ B -> (Fun B -> Fun A))
3	1, 2	anim12i 536	. . 3 |- ((B C_ A /\ A C_ B) -> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
4	3	ancoms 416	. 2 |- ((A C_ B /\ B C_ A) -> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
5		eqss 2860	. 2 |- (A = B <-> (A C_ B /\ B C_ A))
6		dfbi2 704	. 2 |- ((Fun A <-> Fun B) <-> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
7	4, 5, 6	3imtr4i 328	1 |- (A = B -> (Fun A <-> Fun B))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   = wceq 1586   C_ wss 2827  Fun wfun 4125

This theorem is referenced by:  funeqi 4545  funeqd 4546  fununi 4582  funcnvuni 4583  cnvresid 4588  fneq1 4602  f1cnvcnv 4699  f1co 4700  f10 4753  fvopab6 4843  funoprabg 5032  tfrlem10 5292  tz7.44lem1 5299  tz7.48-2OLD 5330  abianfp 5338  th3qcor 5536  elpm 5556  ssdomg 5628  fndmeng 5649  sbthlem7 5682  sbthlem8 5683  ordtypelem4 5918  tz9.12lem2 6007  tz9.12lem3 6008  axdc3lem2 6306  zorn2lem4 6364  axaddopr 6783  axmulopr 6784  idcn 9908  fungid 10208  vsfval 10455  ajfuni 10730  dfrelog 10981  funadj 12282  funcnvadj 12286  bnj1379 13871  bnj1385 13873  bnj1375 14280  bnj1497 14331  injrec2 15178  cmpfun 15214  repfuntw 15241  cur1val 15285  isalg 15862  algi 15868  tartarmap 16075  ordtypelem4OLD 16202  neibastop2lem1 16343  neibastop2lem3 16345  neibastop2lem4 16346

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-br 3508  df-opab 3566  df-id 3747  df-rel 4134  df-cnv 4135  df-co 4136  df-fun 4141

Copyright terms: Public domain