![]() |
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 2748 | . . 3 ⊢ (𝐴 = 𝐵 → (ran 𝐹 = 𝐴 ↔ ran 𝐹 = 𝐵)) | |
2 | 1 | anbi2d 629 | . 2 ⊢ (𝐴 = 𝐵 → ((𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴) ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵))) |
3 | df-fo 6502 | . 2 ⊢ (𝐹:𝐶–onto→𝐴 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐴)) | |
4 | df-fo 6502 | . 2 ⊢ (𝐹:𝐶–onto→𝐵 ↔ (𝐹 Fn 𝐶 ∧ ran 𝐹 = 𝐵)) | |
5 | 2, 3, 4 | 3bitr4g 313 | 1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ran crn 5634 Fn wfn 6491 –onto→wfo 6494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-fo 6502 |
This theorem is referenced by: fimadmfo 6765 f1oeq3 6774 foeq123d 6777 resdif 6805 ncanth 7311 ffoss 7878 rneqdmfinf1o 9272 fidomdm 9273 fifo 9368 brwdom 9503 brwdom2 9509 canthwdom 9515 ixpiunwdom 9526 fin1a2lem7 10342 dmct 10460 znnen 16094 quslem 17425 znzrhfo 20954 rncmp 22747 connima 22776 conncn 22777 qtopcmplem 23058 qtoprest 23068 eupths 29144 pjhfo 30648 2ndresdjuf1o 31566 cycpmconjvlem 31990 msrfo 34140 ivthALT 34807 bj-inftyexpitaufo 35673 poimirlem26 36104 poimirlem27 36105 opidon2OLD 36313 founiiun0 43399 focofob 45302 fundcmpsurinj 45591 fundcmpsurbijinj 45592 fullthinc 47056 |
Copyright terms: Public domain | W3C validator |