Theorem feq1 6634

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 6577	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5882	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3969	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6490	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6490	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3905  ran crn 5624   Fn wfn 6481  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  feq1d  6638  feq1i  6647  elimf  6655  f00  6710  f0bi  6711  f0dom0  6712  fconstg  6715  f1eq1  6719  fprb  7134  fconst2g  7143  fsnex  7224  orderseqlem  8097  soseq  8099  elmapg  8773  mapfset  8784  fsetsspwxp  8787  fsetfcdm  8794  fsetfocdm  8795  fsetprcnex  8796  ac6sfi  9189  updjud  9849  ac5num  9949  acni2  9959  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  coftr  10186  alephsing  10189  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3  10367  axdc4lem  10368  ac6num  10392  inar1  10688  axdc4uzlem  13908  seqf1olem2  13967  seqf1o  13968  iswrd  14440  cshf1  14734  wrdlen2i  14867  ramub2  16944  ramcl  16959  isacs2  17577  isacs1i  17581  mreacs  17582  mgmb1mgm1  18547  elefmndbas2  18766  isgrpinv  18890  isghm  19112  isghmOLD  19113  islindf  21737  psdmul  22069  mat1dimelbas  22374  1stcfb  23348  upxp  23526  txcn  23529  isi1f  25591  mbfi1fseqlem6  25637  mbfi1flimlem  25639  itg2addlem  25675  plyf  26119  elno  27573  elnoOLD  27574  griedg0prc  29227  isgrpo  30459  vciOLD  30523  isvclem  30539  isnvlem  30572  ajmoi  30820  ajval  30823  hlimi  31150  chlimi  31196  chcompl  31204  adjmo  31794  adjeu  31851  adjval  31852  adj1  31895  adjeq  31897  cnlnssadj  32042  pjinvari  32153  padct  32676  locfinref  33807  isrnmeas  34166  filnetlem4  36354  bj-finsumval0  37258  poimirlem25  37624  poimirlem28  37627  volsupnfl  37644  mbfresfi  37645  upixp  37708  sdclem2  37721  sdclem1  37722  fdc  37724  ismgmOLD  37829  elghomlem2OLD  37865  istendo  40739  sticksstones1  42119  sticksstones2  42120  sticksstones3  42121  sticksstones8  42126  sticksstones9  42127  sticksstones10  42128  sticksstones11  42129  sticksstones12a  42130  sticksstones12  42131  sticksstones15  42134  sticksstones17  42136  sticksstones18  42137  sticksstones19  42138  sn-isghm  42646  ismrc  42674  relpeq1  44918  fmuldfeqlem1  45564  fmuldfeq  45565  dvnprodlem1  45928  stoweidlem15  45997  stoweidlem16  45998  stoweidlem17  45999  stoweidlem19  46001  stoweidlem20  46002  stoweidlem21  46003  stoweidlem22  46004  stoweidlem23  46005  stoweidlem27  46009  stoweidlem31  46013  stoweidlem32  46014  stoweidlem42  46024  stoweidlem48  46030  stoweidlem51  46033  stoweidlem59  46041  isomenndlem  46512  smfpimcclem  46789  fsetsniunop  47034  cfsetsnfsetf  47043  cfsetsnfsetf1  47044  cfsetsnfsetfo  47045  lincdifsn  48410  0aryfvalel  48620  mof0ALT  48825  mofsn  48829