Theorem funeq 3521

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 3520	. . . 4 |- (B (_ A -> (Fun A -> Fun B))
2		funss 3520	. . . 4 |- (A (_ B -> (Fun B -> Fun A))
3	1, 2	anim12i 333	. . 3 |- ((B (_ A /\ A (_ B) -> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
4	3	ancoms 436	. 2 |- ((A (_ B /\ B (_ A) -> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
5		eqss 2067	. 2 |- (A = B <-> (A (_ B /\ B (_ A))
6		bi 513	. 2 |- ((Fun A <-> Fun B) <-> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
7	4, 5, 6	3imtr4 219	1 |- (A = B -> (Fun A <-> Fun B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   (_ wss 2037  Fun wfun 3166

This theorem is referenced by:  funopg 3533  fununi 3549  funcnvuni 3550  cnvresid 3555  fneq1 3568  f1eq1 3645  f1cnv 3651  f1co 3652  f10 3698  f1oi 3702  tfrlem10 3905  tz7.44lem1 3912  tz7.48-2 3942  abianfp 3947  funoprabg 3995  th3qcor 4300  elpm 4320  ssdomg 4389  sbthlem7 4433  sbthlem8 4434  tz9.12lem2 4632  tz9.12lem3 4633  zorn2lem4 4763  axaddopr 5237  axmulopr 5238  idcn 7705  vsfval 8194  ajfuni 8451  ajfun 8452  dfrelog 8678  funadj 9730  funcnvadj 9734  cmpfun 10363  isalg 10497  algi 10504

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-opab 2657  df-id 2824  df-rel 3175  df-cnv 3176  df-co 3177  df-fun 3182

Copyright terms: Public domain