![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > foeq3 | Structured version Visualization version GIF version |
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
foeq3 | ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2836 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 622 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))) |
3 | df-fo 6129 | . 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴)) | |
4 | df-fo 6129 | . 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 306 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1656 ran crn 5343 Fn wfn 6118 –onto→wfo 6121 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 df-cleq 2818 df-fo 6129 |
This theorem is referenced by: fimadmfo 6362 f1oeq3 6369 foeq123d 6372 resdif 6398 ffoss 7389 rneqdmfinf1o 8511 fidomdm 8512 fifo 8607 brwdom 8741 brwdom2 8747 canthwdom 8753 ixpiunwdom 8765 fin1a2lem7 9543 dmct 9661 znnen 15315 quslem 16556 znzrhfo 20255 rncmp 21570 connima 21599 conncn 21600 qtopcmplem 21881 qtoprest 21891 eupths 27565 pjhfo 29109 msrfo 31978 ivthALT 32857 bj-inftyexpitaufo 33621 poimirlem26 33972 poimirlem27 33973 opidon2OLD 34188 founiiun0 40178 |
Copyright terms: Public domain | W3C validator |