![]() |
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 6773 | . . 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 6774 | . . 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 6775 | . . 3 ⊢ (𝐶 = 𝐷 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) | |
9 | 7, 8 | syl 17 | . 2 ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
10 | 3, 6, 9 | 3bitrd 305 | 1 ⊢ (𝜑 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐺:𝐵–1-1-onto→𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 –1-1-onto→wf1o 6496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-br 5107 df-opab 5169 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 |
This theorem is referenced by: f1oprswap 6829 f1oprg 6830 f1ossf1o 7075 cnfcom 9637 ackbij2lem2 10177 idffth 17821 ressffth 17826 symgval 19151 symg1bas 19173 symg2bas 19175 symgfixels 19217 symgfixelsi 19218 rhmf1o 20165 mat1f1o 21830 ushgredgedg 28180 ushgredgedgloop 28182 trlreslem 28650 wlknwwlksnbij 28836 wwlksnextbij 28850 clwlknf1oclwwlkn 29031 eupth0 29161 eupthp1 29163 foresf1o 31434 f1ocnt 31708 symgcom 31937 cycpmcl 31968 cycpmconjslem2 32007 nsgqusf1o 32197 dimkerim 32325 indf1ofs 32628 eulerpartgbij 32975 eulerpartlemn 32984 reprpmtf1o 33242 poimirlem16 36097 poimirlem17 36098 poimirlem19 36100 poimirlem20 36101 poimirlem28 36109 metakunt17 40596 wessf1ornlem 43410 disjf1o 43417 ssnnf1octb 43421 sge0fodjrnlem 44664 f1oresf1orab 45528 isomgr 46022 rnghmf1o 46208 |
Copyright terms: Public domain | W3C validator |