Theorem feq1 6684

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Proof of Theorem feq1

Step	Hyp	Ref	Expression
1		fneq1 6627	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5924	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3965	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6541	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6541	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3902  ran crn 5660   Fn wfn 6532  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  feq1d  6688  feq1i  6697  elimf  6705  f00  6761  f0bi  6762  f0dom0  6763  fconstg  6766  f1eq1  6770  fprb  7196  fconst2g  7206  fsnex  7288  orderseqlem  8159  soseq  8161  elmapg  8842  mapfset  8855  fsetsspwxp  8858  fsetfcdm  8865  fsetfocdm  8866  fsetprcnex  8867  ac6sfi  9258  updjud  9943  ac5num  10043  acni2  10053  cofsmo  10275  cfsmolem  10276  cfcoflem  10278  coftr  10279  alephsing  10282  axdc2lem  10454  axdc3lem2  10457  axdc3lem3  10458  axdc3  10460  axdc4lem  10461  ac6num  10485  inar1  10788  axdc4uzlem  14051  seqf1olem2  14110  seqf1o  14111  iswrd  14584  cshf1  14885  wrdlen2i  15017  ramub2  17112  ramcl  17127  isacs2  17747  isacs1i  17751  mreacs  17752  mgmb1mgm1  18753  elefmndbas2  18989  isgrpinv  19123  isghm  19349  islindf  22031  psdmul  22400  mat1dimelbas  22699  1stcfb  23676  upxp  23855  txcn  23858  isi1f  25908  mbfi1fseqlem6  25954  mbfi1flimlem  25956  itg2addlem  25992  plyf  26430  elno  27890  griedg0prc  29732  isgrpo  30986  vciOLD  31050  isvclem  31066  isnvlem  31099  ajmoi  31347  ajval  31350  hlimi  31677  chlimi  31723  chcompl  31731  adjmo  32321  adjeu  32378  adjval  32379  adj1  32422  adjeq  32424  cnlnssadj  32569  pjinvari  32680  padct  33197  locfinref  34359  isrnmeas  34719  filnetlem4  37008  bj-finsumval0  38045  poimirlem25  38402  poimirlem28  38405  volsupnfl  38422  mbfresfi  38423  upixp  38487  sdclem2  38500  sdclem1  38501  fdc  38503  ismgmOLD  38608  elghomlem2OLD  38644  istendo  41641  sticksstones1  43020  sticksstones2  43021  sticksstones3  43022  sticksstones8  43027  sticksstones9  43028  sticksstones10  43029  sticksstones11  43030  sticksstones12a  43031  sticksstones12  43032  sticksstones15  43035  sticksstones17  43037  sticksstones18  43038  sticksstones19  43039  sn-isghm  43527  ismrc  43554  relpeq1  45775  fmuldfeqlem1  46420  fmuldfeq  46421  dvnprodlem1  46782  stoweidlem15  46851  stoweidlem16  46852  stoweidlem17  46853  stoweidlem19  46855  stoweidlem20  46856  stoweidlem21  46857  stoweidlem22  46858  stoweidlem23  46859  stoweidlem27  46863  stoweidlem31  46867  stoweidlem32  46868  stoweidlem42  46878  stoweidlem48  46884  stoweidlem51  46887  stoweidlem59  46895  isomenndlem  47366  smfpimcclem  47643  fsetsniunop  47945  cfsetsnfsetf  47954  cfsetsnfsetf1  47955  cfsetsnfsetfo  47956  lincdifsn  49362  0aryfvalel  49572  mof0ALT  49776  mofsn  49780