f1eq1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1eq1		Structured version Visualization version GIF version

Theorem f1eq1 6661

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)

**Assertion**
Ref	Expression
f1eq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

**Proof of Theorem f1eq1**
Step	Hyp	Ref	Expression
1		feq1 6577	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
2		cnveq 5779	. . . 4 ⊢ (𝐹 = 𝐺 → ^◡𝐹 = ^◡𝐺)
3	2	funeqd 6452	. . 3 ⊢ (𝐹 = 𝐺 → (Fun ^◡𝐹 ↔ Fun ^◡𝐺))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺)))
5		df-f1 6435	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ^◡𝐹))
6		df-f1 6435	. 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ^◡𝐺))
7	4, 5, 6	3bitr4g 313	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1541 ^◡ccnv 5587 Fun wfun 6424 ⟶wf 6426 –1-1→wf1 6427

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-ext 2710

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-sb 2071 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-v 3432 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-sn 4567 df-pr 4569 df-op 4573 df-br 5079 df-opab 5141 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-fun 6432 df-fn 6433 df-f 6434 df-f1 6435

This theorem is referenced by: f1oeq1 6700 f1eq123d 6704 fo00 6747 f1prex 7149 f1iun 7773 tposf12 8051 oacomf1olem 8371 f1dom3g 8726 f1dom2gOLD 8729 f1domg 8731 dom3d 8753 domtr 8764 domssex2 8889 1sdom 8987 marypha1lem 9153 fseqenlem1 9764 dfac12lem2 9884 dfac12lem3 9885 ackbij2 9983 fin23lem28 10080 fin23lem32 10084 fin23lem34 10086 fin23lem35 10087 fin23lem41 10092 iundom2g 10280 pwfseqlem5 10403 hashf1lem1 14149 hashf1lem1OLD 14150 hashf1lem2 14151 hashf1 14152 4sqlem11 16637 injsubmefmnd 18517 conjsubgen 18848 sylow1lem2 19185 sylow2blem1 19206 hauspwpwf1 23119 istrkg2ld 26802 axlowdim 27310 sizusglecusg 27811 specval 30239 aciunf1lem 30978 zrhchr 31905 qqhre 31949 eldioph2lem2 40563 meadjiunlem 43957 fcoresf1b 44515 fundcmpsurbijinjpreimafv 44811 fundcmpsurinjpreimafv 44812 fundcmpsurinjimaid 44815 f1sn2g 46130 f102g 46131