![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oeq123d | Structured version Visualization version GIF version |
Description: Equality deduction for one-to-one onto functions. (Contributed by Mario Carneiro, 27-Jan-2017.) |
Ref | Expression |
---|---|
f1eq123d.1 | ⊢ (𝜑 → 𝐹 = 𝐺) |
f1eq123d.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
f1eq123d.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
f1oeq123d | ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1eq123d.1 | . . 3 ⊢ (𝜑 → 𝐹 = 𝐺) | |
2 | f1oeq1 6269 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐴–1-1-onto→𝐶)) |
4 | f1eq123d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
5 | f1oeq2 6270 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶)) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐶)) |
7 | f1eq123d.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
8 | f1oeq3 6271 | . . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
10 | 3, 6, 9 | 3bitrd 294 | 1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1631 –1-1-onto→wf1o 6031 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-rab 3070 df-v 3353 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-br 4788 df-opab 4848 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-fun 6034 df-fn 6035 df-f 6036 df-f1 6037 df-fo 6038 df-f1o 6039 |
This theorem is referenced by: f1oprswap 6322 f1oprg 6323 f1ossf1o 6539 cnfcom 8762 ackbij2lem2 9265 s2f1o 13871 s4f1o 13873 idffth 16801 ressffth 16806 symg1bas 18024 symg2bas 18026 symgfixels 18062 symgfixelsi 18063 rhmf1o 18943 mat1f1o 20503 isismt 25651 ushgredgedg 26344 ushgredgedgloop 26346 ushgredgedgloopOLD 26347 trlreslem 26832 wlknwwlksnbij 27027 wwlksnextbij 27047 clwlknf1oclwwlkn 27256 eupth0 27395 eupthp1 27397 clwwlknonclwlknonf1oOLD 27552 dlwwlknondlwlknonf1oOLD 27557 foresf1o 29682 f1ocnt 29900 indf1ofs 30429 eulerpartgbij 30775 eulerpartlemn 30784 reprpmtf1o 31045 poimirlem16 33759 poimirlem17 33760 poimirlem19 33762 poimirlem20 33763 poimirlem28 33771 wessf1ornlem 39892 disjf1o 39899 ssnnf1octb 39903 sge0fodjrnlem 41151 f1oresf1orab 41832 rnghmf1o 42432 |
Copyright terms: Public domain | W3C validator |