Theorem feq1 6490

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 6439	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5801	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3998	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6354	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6354	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ⊆ wss 3936  ran crn 5551   Fn wfn 6345  ⟶wf 6346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-br 5060  df-opab 5122  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-fun 6352  df-fn 6353  df-f 6354

This theorem is referenced by:  feq1d  6494  feq1i  6500  elimf  6508  f00  6556  f0bi  6557  f0dom0  6558  fconstg  6561  f1eq1  6565  fprb  6951  fconst2g  6960  fsnex  7033  elmapg  8413  ac6sfi  8756  updjud  9357  ac5num  9456  acni2  9466  cofsmo  9685  cfsmolem  9686  cfcoflem  9688  coftr  9689  alephsing  9692  axdc2lem  9864  axdc3lem2  9867  axdc3lem3  9868  axdc3  9870  axdc4lem  9871  ac6num  9895  inar1  10191  axdc4uzlem  13345  seqf1olem2  13404  seqf1o  13405  iswrd  13857  cshf1  14166  wrdlen2i  14298  ramub2  16344  ramcl  16359  isacs2  16918  isacs1i  16922  mreacs  16923  mgmb1mgm1  17859  elefmndbas2  18033  isgrpinv  18150  isghm  18352  islindf  20950  mat1dimelbas  21074  1stcfb  22047  upxp  22225  txcn  22228  isi1f  24269  mbfi1fseqlem6  24315  mbfi1flimlem  24317  itg2addlem  24353  plyf  24782  griedg0prc  27040  isgrpo  28268  vciOLD  28332  isvclem  28348  isnvlem  28381  ajmoi  28629  ajval  28632  hlimi  28959  chlimi  29005  chcompl  29013  adjmo  29603  adjeu  29660  adjval  29661  adj1  29704  adjeq  29706  cnlnssadj  29851  pjinvari  29962  padct  30449  locfinref  31100  isrnmeas  31454  orderseqlem  33089  soseq  33091  elno  33148  filnetlem4  33724  bj-finsumval0  34561  poimirlem25  34911  poimirlem28  34914  volsupnfl  34931  mbfresfi  34932  upixp  34998  sdclem2  35011  sdclem1  35012  fdc  35014  ismgmOLD  35122  elghomlem2OLD  35158  istendo  37890  ismrc  39291  fmuldfeqlem1  41855  fmuldfeq  41856  dvnprodlem1  42223  stoweidlem15  42293  stoweidlem16  42294  stoweidlem17  42295  stoweidlem19  42297  stoweidlem20  42298  stoweidlem21  42299  stoweidlem22  42300  stoweidlem23  42301  stoweidlem27  42305  stoweidlem31  42309  stoweidlem32  42310  stoweidlem42  42320  stoweidlem48  42326  stoweidlem51  42329  stoweidlem59  42337  isomenndlem  42805  smfpimcclem  43074  lincdifsn  44472