Theorem feq1 6665

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 6608	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5910	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3967	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 641	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6521	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6521	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ⊆ wss 3904  ran crn 5646   Fn wfn 6512  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  feq1d  6669  feq1i  6678  elimf  6686  f00  6742  f0bi  6743  f0dom0  6744  fconstg  6747  f1eq1  6751  fprb  7174  fconst2g  7183  fsnex  7263  orderseqlem  8132  soseq  8134  elmapg  8816  mapfset  8827  fsetsspwxp  8830  fsetfcdm  8837  fsetfocdm  8838  fsetprcnex  8839  ac6sfi  9224  updjud  9889  ac5num  9989  acni2  9999  cofsmo  10223  cfsmolem  10224  cfcoflem  10226  coftr  10227  alephsing  10230  axdc2lem  10402  axdc3lem2  10405  axdc3lem3  10406  axdc3  10408  axdc4lem  10409  ac6num  10433  inar1  10730  axdc4uzlem  13993  seqf1olem2  14052  seqf1o  14053  iswrd  14525  cshf1  14820  wrdlen2i  14952  ramub2  17033  ramcl  17048  isacs2  17668  isacs1i  17672  mreacs  17673  mgmb1mgm1  18672  elefmndbas2  18891  isgrpinv  19018  isghm  19239  islindf  21844  psdmul  22211  mat1dimelbas  22511  1stcfb  23485  upxp  23663  txcn  23666  isi1f  25716  mbfi1fseqlem6  25762  mbfi1flimlem  25764  itg2addlem  25800  plyf  26238  elno  27687  griedg0prc  29411  isgrpo  30646  vciOLD  30710  isvclem  30726  isnvlem  30759  ajmoi  31007  ajval  31010  hlimi  31337  chlimi  31383  chcompl  31391  adjmo  31981  adjeu  32038  adjval  32039  adj1  32082  adjeq  32084  cnlnssadj  32229  pjinvari  32340  padct  32870  locfinref  34099  isrnmeas  34458  filnetlem4  36705  bj-finsumval0  37741  poimirlem25  38108  poimirlem28  38111  volsupnfl  38128  mbfresfi  38129  upixp  38192  sdclem2  38205  sdclem1  38206  fdc  38208  ismgmOLD  38313  elghomlem2OLD  38349  istendo  41348  sticksstones1  42727  sticksstones2  42728  sticksstones3  42729  sticksstones8  42734  sticksstones9  42735  sticksstones10  42736  sticksstones11  42737  sticksstones12a  42738  sticksstones12  42739  sticksstones15  42742  sticksstones17  42744  sticksstones18  42745  sticksstones19  42746  sn-isghm  43219  ismrc  43246  relpeq1  45484  fmuldfeqlem1  46122  fmuldfeq  46123  dvnprodlem1  46484  stoweidlem15  46553  stoweidlem16  46554  stoweidlem17  46555  stoweidlem19  46557  stoweidlem20  46558  stoweidlem21  46559  stoweidlem22  46560  stoweidlem23  46561  stoweidlem27  46565  stoweidlem31  46569  stoweidlem32  46570  stoweidlem42  46580  stoweidlem48  46586  stoweidlem51  46589  stoweidlem59  46597  isomenndlem  47068  smfpimcclem  47345  fsetsniunop  47607  cfsetsnfsetf  47616  cfsetsnfsetf1  47617  cfsetsnfsetfo  47618  lincdifsn  49010  0aryfvalel  49220  mof0ALT  49425  mofsn  49429