Theorem fneq1 5674

Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fneq1

Proof of Theorem fneq1

Step	Hyp	Ref	Expression
1		funeq 5612	. . 3
2		dmeq 5208	. . . 4
3	2	eqeq1d 2459	. . 3
4	1, 3	anbi12d 710	. 2
5		df-fn 5596	. 2
6		df-fn 5596	. 2
7	4, 5, 6	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  domcdm 5004  Funwfun 5587  Fnwfn 5588

This theorem is referenced by:  fneq1d  5676  fneq1i  5680  fn0  5705  feq1  5718  foeq1  5796  f1ocnv  5833  dffn5  5918  mpteqb  5970  fnsnb  6090  fnprb  6129  fnprOLD  6130  eufnfv  6146  tfrlem12  7077  mapval2  7468  elixp2  7493  ixpfn  7495  elixpsn  7528  inf3lem6  8071  aceq3lem  8522  dfac4  8524  dfacacn  8542  axcc2lem  8837  axcc3  8839  seqof  12164  ccatvalfn  12599  swrdvalfn  12663  cshword  12762  0csh0  12764  rrgsupp  17939  elpt  20073  elptr  20074  ptcmplem3  20554  prdsxmslem2  21032  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  fnchoice  31404  dfafn5b  32246  rngchomffvalOLD  32803  bnj62  33773  bnj976  33836  bnj66  33918  bnj124  33929  bnj607  33974  bnj873  33982  bnj1234  34069  bnj1463  34111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-fun 5595  df-fn 5596