Theorem funeq 3610

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 3609	. . . 4 |- (B (_ A -> (Fun A -> Fun B))
2		funss 3609	. . . 4 |- (A (_ B -> (Fun B -> Fun A))
3	1, 2	anim12i 331	. . 3 |- ((B (_ A /\ A (_ B) -> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
4	3	ancoms 438	. 2 |- ((A (_ B /\ B (_ A) -> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
5		eqss 2121	. 2 |- (A = B <-> (A (_ B /\ B (_ A))
6		dfbi2 516	. 2 |- ((Fun A <-> Fun B) <-> ((Fun A -> Fun B) /\ (Fun B -> Fun A)))
7	4, 5, 6	3imtr4i 217	1 |- (A = B -> (Fun A <-> Fun B))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 988   (_ wss 2091  Fun wfun 3231

This theorem is referenced by:  funopg 3622  fununi 3638  funcnvuni 3639  cnvresid 3644  fneq1 3657  f1eq1 3735  f1cnv 3741  f1co 3742  f10 3789  f1oi 3793  tfrlem10 3996  tz7.44lem1 4003  tz7.48-2 4033  abianfp 4038  funoprabg 4087  th3qcor 4403  elpm 4423  ssdomg 4495  sbthlem7 4540  sbthlem8 4541  tz9.12lem2 4746  tz9.12lem3 4747  zorn2lem4 4877  axaddopr 5354  axmulopr 5355  idcn 7886  vsfval 8373  ajfuni 8639  ajfun 8640  dfrelog 8875  funadj 9931  funcnvadj 9935  cmpfun 10585  isalg 10788  algi 10795

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-opab 2718  df-id 2889  df-rel 3240  df-cnv 3241  df-co 3242  df-fun 3247

Copyright terms: Public domain