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 5880	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3962	. . 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 1541   ⊆ wss 3898  ran crn 5620   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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  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  7223  orderseqlem  8093  soseq  8095  elmapg  8769  mapfset  8780  fsetsspwxp  8783  fsetfcdm  8790  fsetfocdm  8791  fsetprcnex  8792  ac6sfi  9175  updjud  9834  ac5num  9934  acni2  9944  cofsmo  10167  cfsmolem  10168  cfcoflem  10170  coftr  10171  alephsing  10174  axdc2lem  10346  axdc3lem2  10349  axdc3lem3  10350  axdc3  10352  axdc4lem  10353  ac6num  10377  inar1  10673  axdc4uzlem  13892  seqf1olem2  13951  seqf1o  13952  iswrd  14424  cshf1  14719  wrdlen2i  14851  ramub2  16928  ramcl  16943  isacs2  17561  isacs1i  17565  mreacs  17566  mgmb1mgm1  18565  elefmndbas2  18784  isgrpinv  18908  isghm  19129  isghmOLD  19130  islindf  21751  psdmul  22082  mat1dimelbas  22387  1stcfb  23361  upxp  23539  txcn  23542  isi1f  25603  mbfi1fseqlem6  25649  mbfi1flimlem  25651  itg2addlem  25687  plyf  26131  elno  27585  elnoOLD  27586  griedg0prc  29244  isgrpo  30479  vciOLD  30543  isvclem  30559  isnvlem  30592  ajmoi  30840  ajval  30843  hlimi  31170  chlimi  31216  chcompl  31224  adjmo  31814  adjeu  31871  adjval  31872  adj1  31915  adjeq  31917  cnlnssadj  32062  pjinvari  32173  padct  32705  locfinref  33875  isrnmeas  34234  filnetlem4  36446  bj-finsumval0  37350  poimirlem25  37705  poimirlem28  37708  volsupnfl  37725  mbfresfi  37726  upixp  37789  sdclem2  37802  sdclem1  37803  fdc  37805  ismgmOLD  37910  elghomlem2OLD  37946  istendo  40879  sticksstones1  42259  sticksstones2  42260  sticksstones3  42261  sticksstones8  42266  sticksstones9  42267  sticksstones10  42268  sticksstones11  42269  sticksstones12a  42270  sticksstones12  42271  sticksstones15  42274  sticksstones17  42276  sticksstones18  42277  sticksstones19  42278  sn-isghm  42791  ismrc  42818  relpeq1  45061  fmuldfeqlem1  45706  fmuldfeq  45707  dvnprodlem1  46068  stoweidlem15  46137  stoweidlem16  46138  stoweidlem17  46139  stoweidlem19  46141  stoweidlem20  46142  stoweidlem21  46143  stoweidlem22  46144  stoweidlem23  46145  stoweidlem27  46149  stoweidlem31  46153  stoweidlem32  46154  stoweidlem42  46164  stoweidlem48  46170  stoweidlem51  46173  stoweidlem59  46181  isomenndlem  46652  smfpimcclem  46929  fsetsniunop  47173  cfsetsnfsetf  47182  cfsetsnfsetf1  47183  cfsetsnfsetfo  47184  lincdifsn  48549  0aryfvalel  48759  mof0ALT  48964  mofsn  48968