Theorem feq1 6686

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 6629	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5929	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3976	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6543	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6543	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ⊆ wss 3913  ran crn 5665   Fn wfn 6534  ⟶wf 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-fun 6541  df-fn 6542  df-f 6543

This theorem is referenced by:  feq1d  6690  feq1i  6699  elimf  6707  f00  6763  f0bi  6764  f0dom0  6765  fconstg  6768  f1eq1  6772  fprb  7195  fconst2g  7204  fsnex  7284  orderseqlem  8155  soseq  8157  elmapg  8838  mapfset  8849  fsetsspwxp  8852  fsetfcdm  8859  fsetfocdm  8860  fsetprcnex  8861  ac6sfi  9246  updjud  9922  ac5num  10022  acni2  10032  cofsmo  10255  cfsmolem  10256  cfcoflem  10258  coftr  10259  alephsing  10262  axdc2lem  10434  axdc3lem2  10437  axdc3lem3  10438  axdc3  10440  axdc4lem  10441  ac6num  10465  inar1  10762  axdc4uzlem  14021  seqf1olem2  14080  seqf1o  14081  iswrd  14554  cshf1  14849  wrdlen2i  14981  ramub2  17076  ramcl  17091  isacs2  17711  isacs1i  17715  mreacs  17716  mgmb1mgm1  18715  elefmndbas2  18935  isgrpinv  19062  isghm  19288  islindf  21933  psdmul  22300  mat1dimelbas  22599  1stcfb  23573  upxp  23751  txcn  23754  isi1f  25804  mbfi1fseqlem6  25850  mbfi1flimlem  25852  itg2addlem  25888  plyf  26326  elno  27778  griedg0prc  29557  isgrpo  30792  vciOLD  30856  isvclem  30872  isnvlem  30905  ajmoi  31153  ajval  31156  hlimi  31483  chlimi  31529  chcompl  31537  adjmo  32127  adjeu  32184  adjval  32185  adj1  32228  adjeq  32230  cnlnssadj  32375  pjinvari  32486  padct  33006  locfinref  34178  isrnmeas  34537  filnetlem4  36817  bj-finsumval0  37854  poimirlem25  38221  poimirlem28  38224  volsupnfl  38241  mbfresfi  38242  upixp  38305  sdclem2  38318  sdclem1  38319  fdc  38321  ismgmOLD  38426  elghomlem2OLD  38462  istendo  41461  sticksstones1  42840  sticksstones2  42841  sticksstones3  42842  sticksstones8  42847  sticksstones9  42848  sticksstones10  42849  sticksstones11  42850  sticksstones12a  42851  sticksstones12  42852  sticksstones15  42855  sticksstones17  42857  sticksstones18  42858  sticksstones19  42859  sn-isghm  43334  ismrc  43361  relpeq1  45582  fmuldfeqlem1  46227  fmuldfeq  46228  dvnprodlem1  46589  stoweidlem15  46658  stoweidlem16  46659  stoweidlem17  46660  stoweidlem19  46662  stoweidlem20  46663  stoweidlem21  46664  stoweidlem22  46665  stoweidlem23  46666  stoweidlem27  46670  stoweidlem31  46674  stoweidlem32  46675  stoweidlem42  46685  stoweidlem48  46691  stoweidlem51  46694  stoweidlem59  46702  isomenndlem  47173  smfpimcclem  47450  fsetsniunop  47712  cfsetsnfsetf  47721  cfsetsnfsetf1  47722  cfsetsnfsetfo  47723  lincdifsn  49126  0aryfvalel  49336  mof0ALT  49540  mofsn  49544