Theorem feq1 6687

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 6630	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5917	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3939	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6542	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6542	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3895  ran crn 5651   Fn wfn 6533  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  feq1d  6691  feq1i  6700  elimf  6708  f00  6764  f0bi  6765  f0dom0  6766  fconstg  6769  f1eq1  6773  fprb  7199  fconst2g  7209  fsnex  7291  orderseqlem  8176  soseq  8178  elmapg  8862  mapfset  8875  fsetsspwxp  8878  fsetfcdm  8885  fsetfocdm  8886  fsetprcnex  8887  ac6sfi  9278  updjud  10018  ac5num  10118  acni2  10128  cofsmo  10350  cfsmolem  10351  cfcoflem  10353  coftr  10354  alephsing  10357  axdc2lem  10529  axdc3lem2  10532  axdc3lem3  10533  axdc3  10535  axdc4lem  10536  ac6num  10560  inar1  10863  axdc4uzlem  14129  seqf1olem2  14188  seqf1o  14189  iswrd  14663  cshf1  14965  wrdlen2i  15098  ramub2  17197  ramcl  17212  isacs2  17832  isacs1i  17836  mreacs  17837  mgmb1mgm1  18838  elefmndbas2  19075  isgrpinv  19209  isghm  19435  islindf  22123  psdmul  22492  mat1dimelbas  22791  1stcfb  23768  upxp  23947  txcn  23950  isi1f  26000  mbfi1fseqlem6  26046  mbfi1flimlem  26048  itg2addlem  26084  plyf  26521  elno  28008  griedg0prc  29850  isgrpo  31104  vciOLD  31168  isvclem  31184  isnvlem  31217  ajmoi  31465  ajval  31468  hlimi  31795  chlimi  31841  chcompl  31849  adjmo  32439  adjeu  32496  adjval  32497  adj1  32540  adjeq  32542  cnlnssadj  32687  pjinvari  32798  padct  33357  locfinref  34519  isrnmeas  34879  filnetlem4  37261  bj-finsumval0  38299  poimirlem25  38656  poimirlem28  38659  volsupnfl  38676  mbfresfi  38677  upixp  38756  sdclem2  38769  sdclem1  38770  fdc  38772  ismgmOLD  38877  elghomlem2OLD  38913  istendo  41910  sticksstones1  43289  sticksstones2  43290  sticksstones3  43291  sticksstones8  43296  sticksstones9  43297  sticksstones10  43298  sticksstones11  43299  sticksstones12a  43300  sticksstones12  43301  sticksstones15  43304  sticksstones17  43306  sticksstones18  43307  sticksstones19  43308  sn-isghm  43777  ismrc  43805  relpeq1  46027  fmuldfeqlem1  46687  fmuldfeq  46688  dvnprodlem1  47049  stoweidlem15  47118  stoweidlem16  47119  stoweidlem17  47120  stoweidlem19  47122  stoweidlem20  47123  stoweidlem21  47124  stoweidlem22  47125  stoweidlem23  47126  stoweidlem27  47130  stoweidlem31  47134  stoweidlem32  47135  stoweidlem42  47145  stoweidlem48  47151  stoweidlem51  47154  stoweidlem59  47162  isomenndlem  47633  smfpimcclem  47910  fsetsniunop  48212  cfsetsnfsetf  48221  cfsetsnfsetf1  48222  cfsetsnfsetfo  48223  lincdifsn  49629  0aryfvalel  49839  mof0ALT  50044  mofsn  50048